From 54eac4f9781d9c07446453697128c4bd036c110d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Jul 2021 16:15:28 -0500 Subject: 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. --- test/regress/regress0/proofs/cyclic-ucp.smt2 | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test/regress/regress0/proofs/cyclic-ucp.smt2 (limited to 'test/regress/regress0') 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) -- cgit v1.2.3