From ec6fe33ab778a7bb5d2d016b799b1918b90fc338 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Jun 2021 10:28:36 -0500 Subject: [PATCH] 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. --- src/smt/proof_manager.cpp | 5 ++--- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/bv/core/bitvec1.smtv1.smt2 | 2 ++ test/regress/regress0/bv/core/bitvec3.smtv1.smt2 | 2 ++ test/regress/regress0/bv/core/constant_core.smt2 | 2 ++ .../regress1/datatypes/dt-param-card4-unsat.smt2 | 1 + test/regress/regress1/hole6.cvc | 1 + .../proofs/issue6625-unsat-core-proofs.smt2 | 16 ++++++++++++++++ .../regress1/proofs/unsat-cores-proofs.smt2 | 10 ++++++++++ test/regress/regress1/sets/sets-disequal.smt2 | 2 +- 10 files changed, 39 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/proofs/issue6625-unsat-core-proofs.smt2 create mode 100644 test/regress/regress1/proofs/unsat-cores-proofs.smt2 diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index ad1e40c77..55cfc1f15 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -130,9 +130,8 @@ void PfManager::setFinalProof(std::shared_ptr 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 daa28580a..860d1854a 100644 --- 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 58cde43c2..78dd44d66 100644 --- 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 bb8c0f7e0..b149c0570 100644 --- 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 a353a5c6f..f9d2e022d 100644 --- 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 29a21a577..1d9b4ef37 100644 --- 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 5ec31d801..c191de6ba 100644 --- 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 index 000000000..e71ae7d92 --- /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 index 000000000..847cd598e --- /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 3acf77108..22cdde8e4 100644 --- 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 -- 2.30.2