More fixes to model generation, with previously failing testcases

Also refactored some header file includes to reduce compile time

2 files changed, 185 insertions, 1 deletions

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index ed810eaeb..e35f24d13 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -18,7 +18,8 @@ TESTS =	\
 	fuzz01.delta01.smt \
 	fuzz02.smt \
 	fuzz03.smt \
-	fuzz04.smt
+	fuzz04.smt \
+	fuzz05.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/auflia/fuzz05.smt b/test/regress/regress0/auflia/fuzz05.smt
new file mode 100644
index 000000000..538f86ece
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz05.smt
@@ -0,0 +1,183 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int Int))
+:extrafuns ((f1 Array Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Int))
+:extrafuns ((v3 Array))
+:formula
+(let (?e4 2)
+(let (?e5 (- v2 v2))
+(let (?e6 (f0 v1 v0))
+(let (?e7 (* ?e6 ?e4))
+(let (?e8 (ite (p0 v2) 1 0))
+(let (?e9 (f1 v3 v3 v3))
+(flet ($e10 (p1 ?e9 v3 v3))
+(flet ($e11 (> ?e7 v1))
+(flet ($e12 (<= ?e8 ?e6))
+(flet ($e13 (p0 ?e8))
+(flet ($e14 (>= v2 v0))
+(flet ($e15 (p0 ?e5))
+(let (?e16 (ite $e12 v3 ?e9))
+(let (?e17 (ite $e15 ?e16 v3))
+(let (?e18 (ite $e11 ?e17 ?e16))
+(let (?e19 (ite $e14 ?e9 ?e9))
+(let (?e20 (ite $e13 ?e16 v3))
+(let (?e21 (ite $e12 v3 ?e19))
+(let (?e22 (ite $e10 ?e16 v3))
+(let (?e23 (ite $e15 ?e5 v0))
+(let (?e24 (ite $e12 v1 ?e6))
+(let (?e25 (ite $e11 ?e6 v0))
+(let (?e26 (ite $e15 ?e25 ?e23))
+(let (?e27 (ite $e12 v1 v0))
+(let (?e28 (ite $e14 ?e23 ?e24))
+(let (?e29 (ite $e10 ?e6 ?e23))
+(let (?e30 (ite $e13 v2 ?e29))
+(let (?e31 (ite $e12 ?e7 ?e25))
+(let (?e32 (ite $e12 ?e8 ?e8))
+(let (?e33 (store v3 ?e27 ?e7))
+(let (?e34 (select ?e21 ?e30))
+(let (?e35 (f1 ?e9 ?e21 ?e18))
+(let (?e36 (f1 ?e9 ?e17 v3))
+(let (?e37 (f1 ?e18 ?e21 ?e19))
+(let (?e38 (f1 ?e33 ?e18 ?e35))
+(let (?e39 (f1 ?e22 ?e22 v3))
+(let (?e40 (f1 ?e18 ?e20 ?e22))
+(let (?e41 (f1 ?e16 ?e33 ?e36))
+(let (?e42 (f0 ?e31 ?e26))
+(let (?e43 (+ ?e25 ?e5))
+(let (?e44 (f0 ?e42 v0))
+(let (?e45 (ite (p0 ?e24) 1 0))
+(let (?e46 (f0 ?e8 v0))
+(let (?e47 (ite (p0 v1) 1 0))
+(let (?e48 (+ ?e23 ?e26))
+(let (?e49 (~ ?e28))
+(let (?e50 (ite (p0 ?e27) 1 0))
+(let (?e51 (~ ?e46))
+(let (?e52 (~ ?e32))
+(let (?e53 (* (~ ?e4) ?e30))
+(let (?e54 (~ ?e29))
+(let (?e55 (- ?e48 ?e31))
+(let (?e56 (* ?e4 ?e7))
+(let (?e57 (f0 ?e29 ?e24))
+(let (?e58 (+ ?e34 v2))
+(let (?e59 (f0 ?e26 ?e50))
+(let (?e60 (f0 ?e6 ?e54))
+(flet ($e61 (p1 ?e38 ?e19 ?e9))
+(flet ($e62 (p1 ?e41 ?e18 ?e40))
+(flet ($e63 (p1 ?e21 ?e35 ?e40))
+(flet ($e64 (p1 ?e16 ?e37 ?e19))
+(flet ($e65 (p1 ?e33 ?e38 ?e18))
+(flet ($e66 (p1 ?e39 ?e20 ?e35))
+(flet ($e67 (p1 ?e38 ?e36 ?e40))
+(flet ($e68 (p1 ?e21 ?e35 ?e20))
+(flet ($e69 (p1 ?e9 ?e33 ?e19))
+(flet ($e70 (p1 ?e18 ?e18 ?e35))
+(flet ($e71 (p1 v3 ?e18 ?e41))
+(flet ($e72 (p1 ?e39 ?e35 v3))
+(flet ($e73 (p1 ?e37 ?e22 ?e38))
+(flet ($e74 (p1 ?e16 ?e9 ?e16))
+(flet ($e75 (p1 ?e17 ?e9 ?e37))
+(flet ($e76 (= ?e53 ?e32))
+(flet ($e77 (>= ?e26 ?e55))
+(flet ($e78 (distinct ?e23 ?e7))
+(flet ($e79 (< ?e28 ?e5))
+(flet ($e80 (<= ?e42 ?e30))
+(flet ($e81 (>= ?e58 ?e50))
+(flet ($e82 (= ?e45 ?e46))
+(flet ($e83 (<= ?e59 ?e32))
+(flet ($e84 (p0 ?e56))
+(flet ($e85 (p0 v2))
+(flet ($e86 (p0 ?e31))
+(flet ($e87 (> ?e25 ?e32))
+(flet ($e88 (= ?e44 ?e54))
+(flet ($e89 (< ?e60 ?e23))
+(flet ($e90 (p0 ?e29))
+(flet ($e91 (distinct v2 ?e6))
+(flet ($e92 (<= ?e59 ?e58))
+(flet ($e93 (= ?e43 ?e47))
+(flet ($e94 (distinct ?e54 v2))
+(flet ($e95 (> ?e8 ?e5))
+(flet ($e96 (distinct ?e59 ?e8))
+(flet ($e97 (distinct ?e48 ?e23))
+(flet ($e98 (> ?e24 ?e60))
+(flet ($e99 (>= ?e34 ?e44))
+(flet ($e100 (< ?e49 ?e7))
+(flet ($e101 (distinct ?e51 ?e53))
+(flet ($e102 (<= ?e52 ?e23))
+(flet ($e103 (<= v1 ?e57))
+(flet ($e104 (>= ?e48 ?e52))
+(flet ($e105 (distinct ?e32 ?e29))
+(flet ($e106 (p0 ?e46))
+(flet ($e107 (<= v0 v0))
+(flet ($e108 (= ?e27 ?e43))
+(flet ($e109 (and $e67 $e107))
+(flet ($e110 (or $e75 $e69))
+(flet ($e111 (implies $e15 $e76))
+(flet ($e112 (xor $e98 $e96))
+(flet ($e113 (and $e78 $e62))
+(flet ($e114 (or $e100 $e77))
+(flet ($e115 (xor $e83 $e12))
+(flet ($e116 (and $e13 $e71))
+(flet ($e117 (xor $e116 $e112))
+(flet ($e118 (not $e86))
+(flet ($e119 (or $e81 $e64))
+(flet ($e120 (iff $e72 $e70))
+(flet ($e121 (iff $e108 $e114))
+(flet ($e122 (or $e88 $e74))
+(flet ($e123 (xor $e105 $e118))
+(flet ($e124 (xor $e103 $e104))
+(flet ($e125 (implies $e93 $e119))
+(flet ($e126 (or $e102 $e90))
+(flet ($e127 (iff $e126 $e89))
+(flet ($e128 (if_then_else $e66 $e109 $e106))
+(flet ($e129 (implies $e85 $e101))
+(flet ($e130 (xor $e110 $e128))
+(flet ($e131 (iff $e63 $e11))
+(flet ($e132 (not $e84))
+(flet ($e133 (not $e68))
+(flet ($e134 (or $e124 $e113))
+(flet ($e135 (if_then_else $e82 $e121 $e94))
+(flet ($e136 (iff $e132 $e80))
+(flet ($e137 (or $e95 $e131))
+(flet ($e138 (and $e129 $e122))
+(flet ($e139 (or $e92 $e135))
+(flet ($e140 (xor $e133 $e139))
+(flet ($e141 (if_then_else $e140 $e91 $e130))
+(flet ($e142 (implies $e117 $e117))
+(flet ($e143 (implies $e14 $e79))
+(flet ($e144 (not $e97))
+(flet ($e145 (and $e120 $e143))
+(flet ($e146 (xor $e134 $e87))
+(flet ($e147 (iff $e125 $e111))
+(flet ($e148 (iff $e147 $e146))
+(flet ($e149 (not $e99))
+(flet ($e150 (or $e145 $e148))
+(flet ($e151 (iff $e149 $e141))
+(flet ($e152 (and $e61 $e61))
+(flet ($e153 (if_then_else $e10 $e142 $e152))
+(flet ($e154 (and $e73 $e115))
+(flet ($e155 (or $e138 $e150))
+(flet ($e156 (and $e127 $e136))
+(flet ($e157 (and $e123 $e137))
+(flet ($e158 (if_then_else $e151 $e155 $e155))
+(flet ($e159 (and $e65 $e153))
+(flet ($e160 (not $e144))
+(flet ($e161 (implies $e156 $e156))
+(flet ($e162 (not $e161))
+(flet ($e163 (if_then_else $e162 $e157 $e159))
+(flet ($e164 (implies $e158 $e154))
+(flet ($e165 (or $e160 $e163))
+(flet ($e166 (not $e164))
+(flet ($e167 (iff $e165 $e165))
+(flet ($e168 (and $e166 $e166))
+(flet ($e169 (and $e168 $e168))
+(flet ($e170 (not $e169))
+(flet ($e171 (iff $e167 $e170))
+$e171
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+