#351: fix Z3 with unsat-cores.

The bug was a redundant call to decRef,
such that Z3 cleaned up a formula that was still in use.
We might actually not require any reference counting in that specific code.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java

@@ -125,22 +125,18 @@ protected Z3Model getEvaluatorWithoutChecks() {
   protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException {
     Preconditions.checkState(!closed);
     long e = creator.extractInfo(f);
-    Native.incRef(z3context, e);
     try {
       if (storedConstraints != null) { // Unsat core generation is on.
         String varName = String.format("Z3_UNSAT_CORE_%d", trackId.getFreshId());
         BooleanFormula t = mgr.getBooleanFormulaManager().makeVariable(varName);
-
         assertContraintAndTrack(e, creator.extractInfo(t));
         storedConstraints.push(storedConstraints.pop().putAndCopy(varName, f));
-        Native.decRef(z3context, e);
       } else {
         assertContraint(e);
       }
     } catch (Z3Exception exception) {
       throw creator.handleZ3Exception(exception);
     }
-    Native.decRef(z3context, e);
     return null;
   }