From 17a09f2cbc7411f38269871e9cdac1569a4b3314 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 14 Jan 2020 20:23:14 -0600
Subject: [PATCH] test: add some regression tests

---
 tests/unsat/diamond2_cong_if.smt2 | 22 ++++++++++++++++++++++
 tests/unsat/if_ff_fg.smt2         | 14 ++++++++++++++
 tests/unsat/nested_if.smt2        | 17 +++++++++++++++++
 tests/unsat/smtlib.626179.smt2    | 14 ++++++++++++++
 tests/unsat/t_subform.smt2        | 12 ++++++++++++
 tests/unsat/test_ite_1.smt2       |  8 ++++++++
 6 files changed, 87 insertions(+)
 create mode 100644 tests/unsat/diamond2_cong_if.smt2
 create mode 100644 tests/unsat/if_ff_fg.smt2
 create mode 100644 tests/unsat/nested_if.smt2
 create mode 100644 tests/unsat/smtlib.626179.smt2
 create mode 100644 tests/unsat/t_subform.smt2
 create mode 100644 tests/unsat/test_ite_1.smt2

diff --git a/tests/unsat/diamond2_cong_if.smt2 b/tests/unsat/diamond2_cong_if.smt2
new file mode 100644
index 00000000..f5149fd1
--- /dev/null
+++ b/tests/unsat/diamond2_cong_if.smt2
@@ -0,0 +1,22 @@
+
+; see diamond2_cong, but using "if"
+; diamond based on congruence, not just transitivity
+(declare-sort a 0)
+(declare-fun x0 () a)
+(declare-fun y0 () a)
+(declare-fun z0 () a)
+(declare-fun p0 () Bool)
+(declare-fun x1 () a)
+(declare-fun y1 () a)
+(declare-fun z1 () a)
+(declare-fun p1 () Bool)
+(declare-fun x2 () a)
+(declare-fun f (a) a)
+(assert (not (= x2 (f (f x0)))))
+(assert (= x1 (f y0)))
+(assert (= x1 (f z0)))
+(assert (= x0 (ite p0 y0 z0)))
+(assert (= x2 (f y1)))
+(assert (= x2 (f z1)))
+(assert (= x1 (ite p1 y1 z1)))
+(check-sat)
diff --git a/tests/unsat/if_ff_fg.smt2 b/tests/unsat/if_ff_fg.smt2
new file mode 100644
index 00000000..6cc85d1c
--- /dev/null
+++ b/tests/unsat/if_ff_fg.smt2
@@ -0,0 +1,14 @@
+
+; if + congruence
+(declare-sort u 0)
+(declare-fun p0 () Bool)
+(declare-fun a () u)
+(declare-fun b1 () u)
+(declare-fun b2 () u)
+(declare-fun c () u)
+(declare-fun f (u) u)
+(assert (= a (ite p0 b1 b2)))
+(assert (= (f b1) c))
+(assert (= (f b2) c))
+(assert (not (= (f a) c)))
+(check-sat)
diff --git a/tests/unsat/nested_if.smt2 b/tests/unsat/nested_if.smt2
new file mode 100644
index 00000000..299d9cd7
--- /dev/null
+++ b/tests/unsat/nested_if.smt2
@@ -0,0 +1,17 @@
+
+; nested ifs
+(declare-sort u 0)
+(declare-fun a () u)
+(declare-fun b () u)
+(declare-fun c () u)
+(declare-fun d () u)
+(declare-fun q0 () Bool)
+(declare-fun q1 () Bool)
+(declare-fun q2 () Bool)
+(declare-fun p (u) Bool)
+(assert (p a))
+(assert (p b))
+(assert (p c))
+(assert (p d))
+(assert (not (p (ite q0 (ite q1 a b) (ite q2 c d)))))
+(check-sat)
diff --git a/tests/unsat/smtlib.626179.smt2 b/tests/unsat/smtlib.626179.smt2
new file mode 100644
index 00000000..95e130c4
--- /dev/null
+++ b/tests/unsat/smtlib.626179.smt2
@@ -0,0 +1,14 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLRA)
+(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 () Real)
+(declare-fun f4 () Real)
+(assert (not (= f1 f2)))
+(assert (not (=> (< f3 f4) (=> (< f4 (* 2.0 f3)) (< 0.0 (- f4 f3))))))
+(check-sat)
+(exit)
diff --git a/tests/unsat/t_subform.smt2 b/tests/unsat/t_subform.smt2
new file mode 100644
index 00000000..d21144ea
--- /dev/null
+++ b/tests/unsat/t_subform.smt2
@@ -0,0 +1,12 @@
+
+(set-info :status "unsat")
+(declare-fun p () Bool)
+(declare-sort u 0)
+(declare-fun f (Bool) u)
+(declare-const a u)
+(declare-const b u)
+(assert (distinct a b))
+
+(assert (= (f p) a))
+(assert (= (f (and p (or p p))) b))
+(check-sat)
diff --git a/tests/unsat/test_ite_1.smt2 b/tests/unsat/test_ite_1.smt2
new file mode 100644
index 00000000..3decfd60
--- /dev/null
+++ b/tests/unsat/test_ite_1.smt2
@@ -0,0 +1,8 @@
+
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun cond () Bool)
+(declare-fun p (U) Bool)
+(assert (and (= a b) (p a) (not (p (ite cond a b)))))
+(check-sat)