diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 24d6ad8be4..38e11fb04c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -88,7 +88,7 @@ public Void addConstraint(BooleanFormula f) throws InterruptedException { public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { if(dump()) { - write("(push)\n"); + write("(push 1)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } @@ -102,7 +102,7 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); writeComment("Original solving time: " + (end - start) + " ms"); - write("(pop)\n"); + write("(pop 1)\n"); } return result; @@ -134,7 +134,7 @@ public Model getModel() throws SolverException { @Override public void push() throws InterruptedException { if(dump()) { - write("(push)\n"); + write("(push 1)\n"); } prover.push(); } @@ -142,7 +142,7 @@ public void push() throws InterruptedException { @Override public void pop() { if(dump()) { - write("(pop)\n"); + write("(pop 1)\n"); } prover.pop(); }