Fix double push (#999)

* Fix double push * Adding test
OCamlPro · Dec 5, 2023 · ba108a6 · ba108a6
1 parent b9ca08f
commit ba108a6
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 2 deletions.
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
@@ -304,8 +304,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
       ~max:n ~elt:(env.res, env.expl) ~init:();
-    Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n);
-    SAT.push env.sat_env n
+    Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n)
 
   let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;

diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.expected b/tests/smtlib/testfile-push-pop2.dolmen.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.smt2 b/tests/smtlib/testfile-push-pop2.dolmen.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(push 1)
+(assert (> x 0))
+(push 1)
+(pop 1)
+(pop 1)
+(assert (< x 0))
+(check-sat)