From 314f57fbaadfd3d3f22d371e16188f5eb80323ed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 21 Jan 2025 14:49:40 -0600 Subject: [PATCH] Do not set dag-thresh to 0 when printing unsat cores (#11549) --- src/proof/unsat_core.cpp | 1 - test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/printer/unsat-core-dagify.smt2 | 10 ++++++++++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/printer/unsat-core-dagify.smt2 diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index f38273a2eca..2c0278a016e 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -51,7 +51,6 @@ UnsatCore::const_iterator UnsatCore::end() const { void UnsatCore::toStream(std::ostream& out) const { options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); Printer::getPrinter(out)->toStream(out, *this); } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 8d2d49dd0d6..3fc04f700eb 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1322,6 +1322,7 @@ set(regress_0_tests regress0/printer/print_unsat_core_lemmas.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc.smt2 + regress0/printer/unsat-core-dagify.smt2 regress0/proj-issue307-get-value-re.smt2 regress0/proj-issue645-abs-value-subs.smt2 regress0/proj-issue750-real-to-int-safe.smt2 diff --git a/test/regress/cli/regress0/printer/unsat-core-dagify.smt2 b/test/regress/cli/regress0/printer/unsat-core-dagify.smt2 new file mode 100644 index 00000000000..b109f2809c4 --- /dev/null +++ b/test/regress/cli/regress0/printer/unsat-core-dagify.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --print-cores-full --produce-unsat-cores +; EXPECT: unsat +; EXPECT: ( +; EXPECT: (let ((_let_1 (> x 0))) (and _let_1 (not _let_1))) +; EXPECT: ) +(set-logic ALL) +(declare-fun x () Int) +(assert (and (> x 0) (not (> x 0)))) +(check-sat) +(get-unsat-core)