diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-14 16:15:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-14 21:15:28 +0000 |
| commit | 54eac4f9781d9c07446453697128c4bd036c110d (patch) | |
| tree | fd9323eb448cd2d45f4d49df72daf09aacb68d96 /test/regress/regress0 | |
| parent | a7d01e2f8f0e2ff5d2af30aa6b97e5e16758997e (diff) | |
Fix for context on input proof generator (#6873)
The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.
This also refactors the debugging traces in this class.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/proofs/cyclic-ucp.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/proofs/cyclic-ucp.smt2 b/test/regress/regress0/proofs/cyclic-ucp.smt2 new file mode 100644 index 000000000..1fe29c262 --- /dev/null +++ b/test/regress/regress0/proofs/cyclic-ucp.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +; EXPECT: unsat +(set-logic ALL) +(push) +(assert (= "A" "")) +(check-sat) +(pop) +(assert (= "" "A")) +(check-sat) |