Do not set dag-thresh to 0 when printing unsat cores (cvc5#11549)

HanielB · Jan 21, 2025 · 314f57f · 314f57f
1 parent 0eb61b1
commit 314f57f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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)