Fix dump models and dump proofs (#4230)

A recent commit (45e489e) made it so that dump-models did not automatically enable produce-models in the global options object, but instead the SmtEngine enabled produce-models internally. The code for dump-models and dump-proofs was (perhaps out of paranoia) checking produce-models and produce-proofs. This removes this check, which is the correct thing to do since SmtEngine internally ensures produce-models is set.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 323f244921494ee3a75e93109890dde9d07d30e1..c5ed54925b3d0004a8e94786f1b98ad3d4e9ca2b 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -148,13 +148,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
-    if (d_options.getProduceModels() && d_options.getDumpModels() &&
-        (res.asSatisfiabilityResult() == Result::SAT ||
-         (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) {
+    if (d_options.getDumpModels()
+        && (res.asSatisfiabilityResult() == Result::SAT
+            || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE)))
+    {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getProof() && d_options.getDumpProofs() &&
-        res.asSatisfiabilityResult() == Result::UNSAT) {
+    if (d_options.getDumpProofs()
+        && res.asSatisfiabilityResult() == Result::UNSAT)
+    {
       getterCommands.emplace_back(new GetProofCommand());
     }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 37776388b9f122f58614e549e14c75bd8da702d0..1f3d4f6231d35c6ecd841b856baaf0685b2d6c05 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -463,6 +463,7 @@ set(regress_0_tests
   regress0/declare-funs.smt2
   regress0/define-fun-model.smt2
   regress0/distinct.smtv1.smt2
+  regress0/simple-dump-model.smt2
   regress0/expect/scrub.01.smtv1.smt2
   regress0/expect/scrub.03.smt2
   regress0/expect/scrub.06.cvc

diff --git a/test/regress/regress0/simple-dump-model.smt2 b/test/regress/regress0/simple-dump-model.smt2
new file mode 100644 (file)
index 0000000..6849b63
--- /dev/null
+++ b/test/regress/regress0/simple-dump-model.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --dump-models
+; EXPECT: sat
+; EXPECT: (model
+; EXPECT: (define-fun x () Int 1)
+; EXPECT: (define-fun y () Int 1)
+; EXPECT: )
+(set-logic QF_LIA)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (and (<= x y) (> x 0)))
+(assert (= y 1))
+(check-sat)