Interpret: error on get-value if in non-sat state

Give an error messge if `get-value` is called, but the solver is not in a satisfiable state. The new behaviour is consistent with `get-models`.
usi-verification-and-security · Apr 20, 2022 · 3b87b53 · 3b87b53
1 parent fecffbf
commit 3b87b53
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/src/bin/Interpret.cc b/src/bin/Interpret.cc
@@ -296,10 +296,12 @@ void Interpret::interp(ASTNode& n) {
                 break;
             }
             case t_getvalue: {
-                if (isInitialized()) {
-                    getValue(n.children);
-                } else {
+                if (not isInitialized()) {
                     notify_formatted(true, "Illegal command before set-logic: get-value");
+                } else if (main_solver->getStatus() != s_True) {
+                    notify_formatted(true, "Command get-value called, but solver is not in SAT state");
+                } else {
+                    getValue(n.children);
                 }
                 break;
             }