diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 2be577eff..c9dc5bd02 100644 --- 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 index a58026e34..35d0ad604 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -204069,6 +204069,27 @@ (package alt-ergo) (action (diff testfile-get-info1.dolmen.expected testfile-get-info1.dolmen_dolmen.output))) + (rule + (target testfile-get-assignment3.err.dolmen_dolmen.output) + (deps (:input testfile-get-assignment3.err.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 1 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-get-assignment3.err.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-get-assignment3.err.dolmen.expected testfile-get-assignment3.err.dolmen_dolmen.output))) (rule (target testfile-get-assignment2.err.dolmen_dolmen.output) (deps (:input testfile-get-assignment2.err.dolmen.smt2)) diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.expected b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected index 6cb130a54..4c0864822 100644 --- a/tests/smtlib/testfile-get-assignment1.err.dolmen.expected +++ b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected @@ -1 +1 @@ -(error "No model produced, cannot execute get-assignment.") +(error "(get-assignment) requires model generation, but it is disabled (try --produce-models)") diff --git a/tests/smtlib/testfile-get-assignment3.err.dolmen.expected b/tests/smtlib/testfile-get-assignment3.err.dolmen.expected new file mode 100644 index 000000000..afd8833ae --- /dev/null +++ b/tests/smtlib/testfile-get-assignment3.err.dolmen.expected @@ -0,0 +1,3 @@ + +unknown +(error "(get-assignment) requires model generation, but it is disabled (try --produce-models)") diff --git a/tests/smtlib/testfile-get-assignment3.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment3.err.dolmen.smt2 new file mode 100644 index 000000000..ad1960cbd --- /dev/null +++ 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) \ No newline at end of file