Uncomment part of the test

test/test_solver.ml

@@ -22,24 +22,33 @@ module Make (M : Mappings_intf.S) = struct
     let symbol_x = Symbol.("x" @: Ty_int) in
     let x = Expr.mk_symbol symbol_x in
     assert_sat (Solver.check solver []);
+
     Solver.push solver;
     Solver.add solver Int.[ x >= int 0 ];
     assert_sat (Solver.check solver []);
     assert (
       let v = Solver.get_value solver x in
       Expr.equal v (int 0) );
     Solver.pop solver 1;
+
     Solver.push solver;
     Solver.add solver [ x = int 3 ];
     assert_sat (Solver.check solver []);
     assert (
       let v = Solver.get_value solver Int.(x * x) in
       Expr.equal v (int 9) );
     Solver.pop solver 1;
-    (* assert_sat (Solver.check solver []);
-       let model = Solver.model ~symbols:[ symbol_x ] solver in
-       let val_x = Option.bind model (fun m -> Model.evaluate m symbol_x) in
-       assert (Option.is_some val_x); *)
+
+    Solver.push solver;
+    Solver.add solver Int.[ x >= int 0 || x < int 0 ];
+    assert_sat (Solver.check solver []);
+    (* necessary, otherwise the solver doesn't know x and can't produce a model
+       for it *)
+    let model = Solver.model ~symbols:[ symbol_x ] solver in
+    let val_x = Option.bind model (fun m -> Model.evaluate m symbol_x) in
+    assert (Option.is_some val_x);
+    Solver.pop solver 1;
+
     Solver.add solver [ x = int 5 ];
     assert_sat (Solver.check solver []);
     let model = Solver.model solver in