From ad8729d3a0060ed635b8a82e9ed323966cc2f49d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Apr 2020 10:52:01 -0500 Subject: [PATCH] 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. --- src/options/options_public_functions.cpp | 4 +++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/dump-unsat-core-full.smt2 | 12 ++++++++++++ 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/dump-unsat-core-full.smt2 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) -- 2.30.2