diff options
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/dump-unsat-core-full.smt2 | 12 |
3 files changed, 16 insertions, 1 deletions
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index a9b8b0714..c7bd1006f 100644 --- 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 7b675d60e..799c23f5a 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/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 index 000000000..3c68501f9 --- /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) |