bug fixes in justification heuristic

* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp

5 files changed, 163 insertions, 3 deletions

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index b098476fc..de3ccd60a 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -22,11 +22,14 @@ TESTS =	\
 	uflia-error0.smt2 \
 	uflia-xs-09-16-3-4-1-5.smt \
 	uflia-xs-09-16-3-4-1-5.delta03.smt \
-	aufbv-fuzz01.smt \	
-	bug347.smt
+	aufbv-fuzz01.smt \
+	bug347.smt \
+	error20.smt \
+	error20.delta01.smt \
+	error122.smt \
+	error122.delta01.smt
 
 # Incorrect answers:
-#	aufbv-fuzz01.smt \
 #
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/decision/error122.delta01.smt b/test/regress/regress0/decision/error122.delta01.smt
new file mode 100644
index 000000000..7c8f930b8
--- /dev/null
+++ b/test/regress/regress0/decision/error122.delta01.smt
@@ -0,0 +1,19 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((v0 BitVec[16]))
+:extrafuns ((a2 Array[16:7]))
+:status sat
+:formula
+(let (?n1 bv0[7])
+(let (?n2 (store a2 v0 ?n1))
+(let (?n3 bv1[16])
+(let (?n4 (select ?n2 ?n3))
+(flet ($n5 (bvult ?n1 ?n4))
+(let (?n6 bv1[1])
+(let (?n7 bv0[1])
+(let (?n8 (ite $n5 ?n6 ?n7))
+(let (?n9 (sign_extend[15] ?n8))
+(flet ($n10 (distinct v0 ?n9))
+(flet ($n11 (not $n10))
+$n11
+))))))))))))
diff --git a/test/regress/regress0/decision/error122.smt b/test/regress/regress0/decision/error122.smt
new file mode 100644
index 000000000..2503ba01e
--- /dev/null
+++ b/test/regress/regress0/decision/error122.smt
@@ -0,0 +1,53 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status unsat
+:extrafuns ((v0 BitVec[16]))
+:extrafuns ((a1 Array[16:4]))
+:extrafuns ((a2 Array[16:7]))
+:formula
+(let (?e3 bv8911[14])
+(let (?e4 (ite (bvsgt (zero_extend[2] ?e3) v0) bv1[1] bv0[1]))
+(let (?e5 (store a2 v0 (extract[13:7] v0)))
+(let (?e6 (store a2 (zero_extend[15] ?e4) (zero_extend[6] ?e4)))
+(let (?e7 (select ?e5 (zero_extend[2] ?e3)))
+(let (?e8 (store ?e5 (sign_extend[2] ?e3) (sign_extend[6] ?e4)))
+(let (?e9 (select a1 v0))
+(let (?e10 (store ?e8 (zero_extend[15] ?e4) (extract[6:0] v0)))
+(let (?e11 (bvadd (zero_extend[6] ?e4) ?e7))
+(let (?e12 (ite (bvult ?e11 ?e7) bv1[1] bv0[1]))
+(let (?e13 (ite (bvult (zero_extend[3] ?e12) ?e9) bv1[1] bv0[1]))
+(let (?e14 (bvlshr (sign_extend[12] ?e9) v0))
+(let (?e15 (ite (= bv1[1] (extract[12:12] ?e3)) ?e14 ?e14))
+(flet ($e16 (bvslt ?e15 v0))
+(flet ($e17 (bvult (sign_extend[15] ?e4) ?e14))
+(flet ($e18 (= (sign_extend[15] ?e12) ?e15))
+(flet ($e19 (distinct (sign_extend[15] ?e12) v0))
+(flet ($e20 (bvugt ?e11 ?e11))
+(flet ($e21 (bvule ?e13 ?e13))
+(flet ($e22 (bvslt ?e15 (sign_extend[9] ?e11)))
+(flet ($e23 (bvslt (zero_extend[9] ?e11) v0))
+(flet ($e24 (bvult v0 (sign_extend[15] ?e12)))
+(flet ($e25 (bvslt ?e7 (sign_extend[6] ?e4)))
+(flet ($e26 (bvule (zero_extend[12] ?e9) ?e15))
+(flet ($e27 (bvuge ?e13 ?e13))
+(flet ($e28 (distinct (zero_extend[6] ?e12) ?e7))
+(flet ($e29 (distinct ?e3 (sign_extend[13] ?e12)))
+(flet ($e30 (xor $e27 $e17))
+(flet ($e31 (or $e25 $e28))
+(flet ($e32 (iff $e31 $e21))
+(flet ($e33 (and $e18 $e22))
+(flet ($e34 (iff $e30 $e33))
+(flet ($e35 (and $e24 $e24))
+(flet ($e36 (and $e29 $e20))
+(flet ($e37 (and $e34 $e26))
+(flet ($e38 (iff $e36 $e16))
+(flet ($e39 (or $e38 $e32))
+(flet ($e40 (not $e19))
+(flet ($e41 (xor $e23 $e35))
+(flet ($e42 (and $e41 $e40))
+(flet ($e43 (implies $e42 $e37))
+(flet ($e44 (not $e43))
+(flet ($e45 (and $e39 $e44))
+$e45
+))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/decision/error20.delta01.smt b/test/regress/regress0/decision/error20.delta01.smt
new file mode 100644
index 000000000..dfa582be9
--- /dev/null
+++ b/test/regress/regress0/decision/error20.delta01.smt
@@ -0,0 +1,19 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((v0 BitVec[16]))
+:extrafuns ((v1 BitVec[1]))
+:extrafuns ((a4 Array[1:7]))
+:status sat
+:formula
+(let (?n1 (select a4 v1))
+(let (?n2 bv0[7])
+(flet ($n3 (bvsle ?n1 ?n2))
+(let (?n4 bv0[16])
+(let (?n5 bv0[1])
+(flet ($n6 (= v1 ?n5))
+(let (?n7 (ite $n6 ?n4 v0))
+(flet ($n8 (= ?n4 ?n7))
+(flet ($n9 (not $n8))
+(flet ($n10 (and $n3 $n9))
+$n10
+)))))))))))
diff --git a/test/regress/regress0/decision/error20.smt b/test/regress/regress0/decision/error20.smt
new file mode 100644
index 000000000..adc638500
--- /dev/null
+++ b/test/regress/regress0/decision/error20.smt
@@ -0,0 +1,66 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status sat
+:extrafuns ((v0 BitVec[16]))
+:extrafuns ((v1 BitVec[1]))
+:extrafuns ((a2 Array[12:10]))
+:extrafuns ((a3 Array[14:11]))
+:extrafuns ((a4 Array[1:7]))
+:formula
+(let (?e5 bv1[1])
+(let (?e6 (ite (= bv1[1] (extract[0:0] v1)) (sign_extend[15] ?e5) v0))
+(let (?e7 (store a4 (extract[4:4] v0) (extract[9:3] v0)))
+(let (?e8 (store ?e7 ?e5 (extract[12:6] v0)))
+(let (?e9 (store ?e8 v1 (sign_extend[6] ?e5)))
+(let (?e10 (select a4 v1))
+(let (?e11 (store ?e8 ?e5 (zero_extend[6] v1)))
+(let (?e12 (select ?e8 v1))
+(let (?e13 (store a2 (extract[14:3] v0) (zero_extend[3] ?e10)))
+(let (?e14 (rotate_right[0] v1))
+(let (?e15 (rotate_right[3] ?e10))
+(let (?e16 (ite (bvsge ?e12 (zero_extend[6] v1)) bv1[1] bv0[1]))
+(let (?e17 (repeat[5] ?e14))
+(let (?e18 (bvsdiv (sign_extend[9] ?e15) ?e6))
+(let (?e19 (bvmul (zero_extend[15] ?e5) v0))
+(flet ($e20 (= (zero_extend[15] ?e5) ?e18))
+(flet ($e21 (bvugt (zero_extend[9] ?e10) ?e19))
+(flet ($e22 (bvsgt ?e15 (zero_extend[6] v1)))
+(flet ($e23 (bvslt ?e14 ?e16))
+(flet ($e24 (bvugt ?e19 (zero_extend[15] v1)))
+(flet ($e25 (distinct ?e12 ?e12))
+(flet ($e26 (bvule ?e17 (sign_extend[4] ?e5)))
+(flet ($e27 (bvsle ?e18 (zero_extend[15] ?e16)))
+(flet ($e28 (bvsle ?e10 ?e15))
+(flet ($e29 (bvsgt ?e12 (zero_extend[6] ?e16)))
+(flet ($e30 (bvsgt (sign_extend[4] ?e5) ?e17))
+(flet ($e31 (bvsle ?e17 (zero_extend[4] ?e14)))
+(flet ($e32 (bvult (zero_extend[11] ?e17) ?e6))
+(flet ($e33 (bvult ?e5 ?e5))
+(flet ($e34 (bvugt ?e12 (sign_extend[2] ?e17)))
+(flet ($e35 (bvsle (sign_extend[6] v1) ?e15))
+(flet ($e36 (bvule ?e15 (zero_extend[6] ?e14)))
+(flet ($e37 (bvsgt v0 ?e6))
+(flet ($e38 (if_then_else $e23 $e25 $e26))
+(flet ($e39 (iff $e33 $e35))
+(flet ($e40 (or $e21 $e36))
+(flet ($e41 (or $e20 $e32))
+(flet ($e42 (and $e22 $e39))
+(flet ($e43 (not $e41))
+(flet ($e44 (implies $e24 $e31))
+(flet ($e45 (or $e42 $e44))
+(flet ($e46 (iff $e27 $e37))
+(flet ($e47 (or $e29 $e46))
+(flet ($e48 (not $e28))
+(flet ($e49 (and $e47 $e43))
+(flet ($e50 (iff $e40 $e30))
+(flet ($e51 (xor $e34 $e50))
+(flet ($e52 (iff $e45 $e51))
+(flet ($e53 (if_then_else $e49 $e49 $e52))
+(flet ($e54 (or $e53 $e38))
+(flet ($e55 (iff $e54 $e54))
+(flet ($e56 (and $e48 $e55))
+(flet ($e57 (and $e56 (not (= ?e6 bv0[16]))))
+(flet ($e58 (and $e57 (not (= ?e6 (bvnot bv0[16])))))
+$e58
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))
+