aboutsummaryrefslogtreecommitdiffstats
path: root/src/lfsc/tests/cvc4_coq40d8ed.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/lfsc/tests/cvc4_coq40d8ed.smt2')
-rw-r--r--src/lfsc/tests/cvc4_coq40d8ed.smt29
1 files changed, 9 insertions, 0 deletions
diff --git a/src/lfsc/tests/cvc4_coq40d8ed.smt2 b/src/lfsc/tests/cvc4_coq40d8ed.smt2
new file mode 100644
index 0000000..29e28b0
--- /dev/null
+++ b/src/lfsc/tests/cvc4_coq40d8ed.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UFLIA)
+(declare-fun op_4 () Int)
+(declare-fun op_1 (Int) Bool)
+(declare-fun op_0 () Int)
+(declare-fun op_2 () Int)
+(declare-fun op_3 (Int) Int)
+(assert (and (= op_2 op_4) (and (= op_0 op_4) (or (not (= (op_3 op_2) (op_3 op_0))) (and (op_1 op_2) (not (op_1 op_0)))))))
+(check-sat)
+(exit)