1 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
new file mode 100644
index 000000000..f0815e8f2
--- /dev/null
+++ b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
@@ -0,0 +1,47 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_UF)
+(set-option :produce-proofs true)
+(set-option :incremental true)
+(declare-fun p () Bool)
+(declare-fun q () Bool)
+
+(push)
+(assert (not (= p (not q))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not q) p)))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not p) (not (not q)))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not q)) (not p))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not p)) (not (not (not q))))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not (not q))) (not (not p)))))
+(assert p)
+(check-sat)
+(pop)
+\ No newline at end of file