From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Apr 2020 20:24:55 +0000 (-0500)
Subject: Fix dump models and dump proofs (#4230)
X-Git-Tag: cvc5-1.0.0~3396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24357fea07bf1eb6b1156a8e455c58faee96b604;p=cvc5.git

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 323f24492..c5ed54925 100644
--- 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 37776388b..1f3d4f623 100644
--- 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
index 000000000..6849b63a8
--- /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)