Fix unsat core proofs (#6655)

Fixes cases of satisfiable unsat cores when proofs are enabled.

Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index ad1e40c77d31478429dc22c6d8e10668acead47b..55cfc1f15b3765953d5bae5aa457a8e6f3faeda0 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -130,9 +130,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
   Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
 
   // Now make the final scope, which ensures that the only open leaves of the
-  // proof are the assertions, unless we are doing proofs to generate unsat
-  // cores, in which case we do not care.
-  d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores());
+  // proof are the assertions.
+  d_finalProof = d_pnm->mkScope(pfn, assertions);
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index daa28580ad294ad6e8e216b1d22d4e851e37f7d8..860d1854ab1ab71fd35f07bd356c68501e1bef6d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1687,9 +1687,11 @@ set(regress_1_tests
   regress1/non-fatal-errors.smt2
   regress1/parsing_ringer.cvc
   regress1/proof00.smt2
+  regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
   regress1/proofs/sat-trivial-cycle.smt2
+  regress1/proofs/unsat-cores-proofs.smt2
   regress1/push-pop/arith_lra_01.smt2
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2

diff --git a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
index 58cde43c2f9d70df3559bd8fcc5b047f0e722291..78dd44d66c799fc23f457d024e97da6e3708d731 100644 (file)
--- a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
+++ b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE:  --no-check-proofs
+; EXPECT: unsat
 (set-option :incremental false)
 (set-info :source "Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
 Contributed by Vijay Ganesh (vganesh@stanford.edu).  Translated into SMT-LIB

diff --git a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
index bb8c0f7e0c7619371a56fb996773608a14475f70..b149c05705b1988bb8c09fc3560fa1dadc2ab64b 100644 (file)
--- a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
+++ b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE:  --no-check-proofs
+; EXPECT: unsat
 (set-option :incremental false)
 (set-info :source "Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
 Contributed by Vijay Ganesh (vganesh@stanford.edu).  Translated into SMT-LIB

diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
index a353a5c6ffba85424527fc87f84deb26d7b483cc..f9d2e022d13cbe48e03f572299dbe72a7fa8ed37 100644 (file)
--- a/test/regress/regress0/bv/core/constant_core.smt2
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE:  --no-check-proofs
+; EXPECT: unsat
 (set-logic QF_BV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2
index 29a21a5778966765e867d853028747005823d247..1d9b4ef375bd1e4f068c553225fa8243d5010997 100644 (file)
--- a/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2
+++ b/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)

diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc
index 5ec31d8016c4bc22e2c4c7449a207ac3a22b3ac6..c191de6bab547d1634d3c37b4bbdcee14f89fe54 100644 (file)
--- a/test/regress/regress1/hole6.cvc
+++ b/test/regress/regress1/hole6.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --no-check-proofs
 % EXPECT: entailed
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;

diff --git a/test/regress/regress1/proofs/issue6625-unsat-core-proofs.smt2 b/test/regress/regress1/proofs/issue6625-unsat-core-proofs.smt2
new file mode 100644 (file)
index 0000000..e71ae7d
--- /dev/null
+++ b/test/regress/regress1/proofs/issue6625-unsat-core-proofs.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const a String)
+(declare-const b String)
+(declare-const c String)
+(push)
+(assert (= (str.++ a b) c))
+(assert (= a "A"))
+(assert (= c ""))
+(check-sat)
+(pop)
+(assert (= (str.++ a b) (str.++ "A" c)))
+(assert (= c (str.++ a b)))
+(check-sat)

diff --git a/test/regress/regress1/proofs/unsat-cores-proofs.smt2 b/test/regress/regress1/proofs/unsat-cores-proofs.smt2
new file mode 100644 (file)
index 0000000..847cd59
--- /dev/null
+++ b/test/regress/regress1/proofs/unsat-cores-proofs.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --produce-proofs -i
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL)
+(push)
+(assert (= "A" ""))
+(check-sat)
+(pop)
+(assert (= "" "A"))
+(check-sat)

diff --git a/test/regress/regress1/sets/sets-disequal.smt2 b/test/regress/regress1/sets/sets-disequal.smt2
index 3acf77108b03e5ebef963ed98f97bfcadcd28aa1..22cdde8e489fe73b2940241796eaef74f17b500d 100644 (file)
--- a/test/regress/regress1/sets/sets-disequal.smt2
+++ b/test/regress/regress1/sets/sets-disequal.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --no-check-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat