diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-11-09 16:35:38 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-09 19:35:38 +0000 |
| commit | 5279adad97c7e85ca36ebc9497fa1b6c801c7ab6 (patch) | |
| tree | 09886464f203aba5c17dcfd1228441b7e52ccd5a /test | |
| parent | a78a1959ae41d2e6f7a93ae77109eec00b39dab6 (diff) | |
[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)
Previously the trivial cycle check only covered the case in which the currently-being-expanded assumption `A` had as its stored proof node `pf` an assumption proof justifying itself. However, it can be the case that `pf` is not an assumption proof, but a proof that nevertheless has `A` as one of its free assumptions. This commit generalizes the trivial cycle check to account for this.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress1/quantifiers/recfact.cvc.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6184-unsat-core.smt2 | 6 |
2 files changed, 10 insertions, 1 deletions
diff --git a/test/regress/regress1/quantifiers/recfact.cvc.smt2 b/test/regress/regress1/quantifiers/recfact.cvc.smt2 index 02676b625..e36707360 100644 --- a/test/regress/regress1/quantifiers/recfact.cvc.smt2 +++ b/test/regress/regress1/quantifiers/recfact.cvc.smt2 @@ -1,4 +1,9 @@ ; EXPECT: unsat +; COMMAND-LINE: +; COMMAND-LINE: --produce-proofs +;; The second command line option, other than the default, is to test +;; unsat core checking with proofs, which at one point had issues for +;; this benchmark due to cycle detection in LazyCDProofChain (set-logic ALL) (set-option :incremental false) (set-option :fmf-fun true) diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2 index 5e257da00..8dcfe81f8 100644 --- a/test/regress/regress1/strings/issue6184-unsat-core.smt2 +++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2 @@ -1,5 +1,9 @@ -; COMMAND-LINE: --strings-exp ; EXPECT: unsat +; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --produce-proofs +;; The second command line option is to test unsat core checking with +;; proofs, which at one point had issues for this benchmark due to +;; cycle detection in LazyCDProofChain (set-logic ALL) (set-info :status unsat) (set-option :check-unsat-cores true) |