Fix dump-unsat-cores-full (#4303)

This adds a fix to ensure dump-unsat-cores-full works by modifying the public options function. This options currently does not work since dumpUnsatCores is only set internally now. This fix is only required until options are refactored so that SmtEngine owns the authoritative copy of options.

diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index a9b8b0714eb9ac482d1cf235329955f5f786ecc2..c7bd1006f4aa444a6179f1be4d16b72b1e4d314b 100644 (file)
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -75,7 +75,9 @@ bool Options::getDumpSynth() const{
 }
 
 bool Options::getDumpUnsatCores() const{
-  return (*this)[options::dumpUnsatCores];
+  // dump unsat cores full enables dumpUnsatCores
+  return (*this)[options::dumpUnsatCores]
+         || (*this)[options::dumpUnsatCoresFull];
 }
 
 bool Options::getEarlyExit() const{

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7b675d60ec33a3d0ead77c4a1980db5fde44c14f..799c23f5ac2d9728d89fa22184258c244385429c 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/dump-unsat-core-full.smt2
   regress0/simple-dump-model.smt2
   regress0/expect/scrub.01.smtv1.smt2
   regress0/expect/scrub.03.smt2

diff --git a/test/regress/regress0/dump-unsat-core-full.smt2 b/test/regress/regress0/dump-unsat-core-full.smt2
new file mode 100644 (file)
index 0000000..3c68501
--- /dev/null
+++ b/test/regress/regress0/dump-unsat-core-full.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: proof
+; COMMAND-LINE: --dump-unsat-cores-full
+; EXPECT: unsat
+; EXPECT: (
+; EXPECT: (and (= x y) (< x y))
+; EXPECT: )
+(set-logic QF_LIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (and (= x y) (< x y)))
+(check-sat)