Adding tests & handling case where model gen is disabled

OCamlPro · Nov 8, 2023 · 7d3b6bd · 7d3b6bd
1 parent 9cbf833
commit 7d3b6bd
Show file tree

Hide file tree

Showing 4 changed files with 52 additions and 15 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -886,22 +886,32 @@ let main () =
 
       | {contents = `Get_assignment; _} ->
         begin
-          match State.get partial_model_key st with
-          | Some Model ((module SAT), partial_model) ->
-            if State.get produce_assignment st then
-              handle_get_assignment
-                ~get_value:(SAT.get_value partial_model)
-                st
-            else
+          if Options.get_interpretation () then begin
+            match State.get partial_model_key st with
+            | Some Model ((module SAT), partial_model) ->
+              if State.get produce_assignment st then
+                handle_get_assignment
+                  ~get_value:(SAT.get_value partial_model)
+                  st
+              else
+                recoverable_error
+                  "Produce assignments disabled; \
+                   add (set-option :produce-assignments true)";
+              st
+            | None ->
+              (* TODO: add the location of the statement. *)
               recoverable_error
-                "Produce assignments disabled; \
-                 add (set-option :produce-assignments true)";
-            st
-          | None ->
-            (* TODO: add the location of the statement. *)
-            recoverable_error
-              "No model produced, cannot execute get-assignment.";
-            st
+                "No model produced, cannot execute get-assignment.";
+              st
+          end
+          else
+            begin
+              (* TODO: add the location of the statement. *)
+              recoverable_error
+                "(get-assignment) requires model generation, \
+                 but it is disabled (try --produce-models)";
+              st
+            end
         end
 
       | {contents = `Other (custom, args); _} ->

diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/smtlib/testfile-get-assignment3.err.dolmen.expected b/tests/smtlib/testfile-get-assignment3.err.dolmen.expected
diff --git a/tests/smtlib/testfile-get-assignment3.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment3.err.dolmen.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-assignments true)
+(declare-const x Int)
+(assert (! (= x 0) :named foo))
+(check-sat)
+(get-assignment)