Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.

4 files changed, 127 insertions, 1 deletions

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index ca3907b0b..45e174026 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -36,7 +36,11 @@ TESTS =	\
 	fc-pigeonhole19.smt2 \
 	Hoare-z3.931718.smt \
 	bug0909.smt2 \
-	lst-no-self-rev-exp.smt2
+	lst-no-self-rev-exp.smt2 \
+	fib-core.smt2 \
+	fore19-exp2-core.smt2 \
+	with-ind-104-core.smt2
+
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/fib-core.smt2 b/test/regress/regress0/fmf/fib-core.smt2
new file mode 100755
index 000000000..e00f19ad4
--- /dev/null
+++ b/test/regress/regress0/fmf/fib-core.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort I_fb 0)
+(declare-fun fb_arg_0_1 (I_fb) Int)
+(declare-fun fb (Int) Int)
+
+(assert (forall ((?j I_fb)) (= (fb (fb_arg_0_1 ?j)) (ite (not (>= (fb_arg_0_1 ?j) 2)) (fb_arg_0_1 ?j) (+ (fb (+ (- 1) (fb_arg_0_1 ?j))) (fb (+ (- 2) (fb_arg_0_1 ?j)))))) ) )
+
+(assert (forall ((?i I_fb)) (ite (not (>= (fb_arg_0_1 ?i) 2)) true (and (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) ) )
+
+(assert (forall ((?i I_fb)) (or (>= (fb_arg_0_1 ?i) 2) (and (not (>= (fb_arg_0_1 ?i) 2)) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) ))
+
+
+(assert (not (= (fb 5) 5)) )
+(assert (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?z) 5)) )))
+
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fore19-exp2-core.smt2 b/test/regress/regress0/fmf/fore19-exp2-core.smt2
new file mode 100755
index 000000000..9a6e1e270
--- /dev/null
+++ b/test/regress/regress0/fmf/fore19-exp2-core.smt2
@@ -0,0 +1,70 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((St (Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St)))
+(Ex (Var!2291 (varID!2292 (_ BitVec 32))))
+(List!2293 (Cons!2294 (head!2295 St) (tail!2296 List!2293)) (Nil!2297))
+))
+(declare-fun error_value!2298 () Bool)
+(declare-fun error_value!2299 () List!2293)
+(declare-fun s () St)
+(declare-fun body!2242_uf_1 (St) St)
+(declare-fun step!2241_uf_2 (St) St)
+(declare-fun init!2239_uf_3 (St) St)
+(declare-fun elze!2246_uf_4 (St) St)
+(declare-fun then!2245_uf_5 (St) St)
+(declare-fun body!2237_uf_6 (St) List!2293)
+(declare-fun tail!2296_uf_7 (List!2293) List!2293)
+(declare-fun head!2295_uf_8 (List!2293) St)
+(declare-fun expr!2240_uf_9 (St) Ex)
+(declare-fun body_uf_10 (St) St)
+(declare-fun expr!2252_uf_11 (St) Ex)
+(declare-fun expr!2244_uf_12 (St) Ex)
+(declare-fun iwf (St) Bool)
+(declare-fun iwfl (List!2293) Bool)
+(declare-fun ewl (St) St)
+(declare-fun ewlList!211 (List!2293) List!2293)
+(declare-sort I_iwf 0)
+(declare-fun iwf_arg_0_13 (I_iwf) St)
+(declare-sort I_iwfl 0)
+(declare-fun iwfl_arg_0_14 (I_iwfl) List!2293)
+(declare-sort I_ewl 0)
+(declare-fun ewl_arg_0_15 (I_ewl) St)
+(declare-sort I_ewlList!211 0)
+(declare-fun ewlList!211_arg_0_16 (I_ewlList!211) List!2293)
+(declare-fun termITE_17 () St)
+(declare-fun termITE_18 () St)
+(declare-fun termITE_19 () St)
+(declare-fun termITE_20 () St)
+
+(assert
+(and
+(forall ((?i1 I_ewl)) (= (ewl (ewl_arg_0_15 ?i1)) 
+
+(ite (is-IfTE (ewl_arg_0_15 ?i1)) (IfTE (ite (is-IfTE (ewl_arg_0_15 ?i1)) (expr!2244 (ewl_arg_0_15 ?i1)) (expr!2244_uf_12 (ewl_arg_0_15 ?i1))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (then!2245 (ewl_arg_0_15 ?i1)) (then!2245_uf_5 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (elze!2246 (ewl_arg_0_15 ?i1)) (elze!2246_uf_4 (ewl_arg_0_15 ?i1))))) 
+
+(ite (is-While (ewl_arg_0_15 ?i1)) (For!2238 Skip!2250 (ite (is-While (ewl_arg_0_15 ?i1)) (expr!2252 (ewl_arg_0_15 ?i1)) (expr!2252_uf_11 (ewl_arg_0_15 ?i1))) Skip!2250 (ewl (ite (is-While (ewl_arg_0_15 ?i1)) (body (ewl_arg_0_15 ?i1)) (body_uf_10 (ewl_arg_0_15 ?i1))))) 
+
+(ite (is-For!2238 (ewl_arg_0_15 ?i1)) (For!2238 (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (init!2239 (ewl_arg_0_15 ?i1)) (init!2239_uf_3 (ewl_arg_0_15 ?i1)))) (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (expr!2240 (ewl_arg_0_15 ?i1)) (expr!2240_uf_9 (ewl_arg_0_15 ?i1))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (step!2241 (ewl_arg_0_15 ?i1)) (step!2241_uf_2 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (body!2242 (ewl_arg_0_15 ?i1)) (body!2242_uf_1 (ewl_arg_0_15 ?i1))))) 
+
+(ewl_arg_0_15 ?i1))))) )
+
+
+(forall ((?i2 I_ewl)) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (then!2245 (ewl_arg_0_15 ?i2)) (then!2245_uf_5 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (elze!2246 (ewl_arg_0_15 ?i2)) (elze!2246_uf_4 (ewl_arg_0_15 ?i2))))) ))) (ite (is-While (ewl_arg_0_15 ?i2)) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-While (ewl_arg_0_15 ?i2)) (body (ewl_arg_0_15 ?i2)) (body_uf_10 (ewl_arg_0_15 ?i2))))) )) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (init!2239 (ewl_arg_0_15 ?i2)) (init!2239_uf_3 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (step!2241 (ewl_arg_0_15 ?i2)) (step!2241_uf_2 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (body!2242 (ewl_arg_0_15 ?i2)) (body!2242_uf_1 (ewl_arg_0_15 ?i2))))) ))) true))) )
+(forall ((?i3 I_iwf)) (= (iwf (iwf_arg_0_13 ?i3)) (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (iwfl (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (body!2237 (iwf_arg_0_13 ?i3)) (body!2237_uf_6 (iwf_arg_0_13 ?i3)))) (ite (is-IfTE (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (elze!2246 (iwf_arg_0_13 ?i3)) (elze!2246_uf_4 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (then!2245 (iwf_arg_0_13 ?i3)) (then!2245_uf_5 (iwf_arg_0_13 ?i3))))) (ite (is-While (iwf_arg_0_13 ?i3)) false (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (body!2242 (iwf_arg_0_13 ?i3)) (body!2242_uf_1 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (step!2241 (iwf_arg_0_13 ?i3)) (step!2241_uf_2 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (init!2239 (iwf_arg_0_13 ?i3)) (init!2239_uf_3 (iwf_arg_0_13 ?i3))))) true))))) ) 
+(forall ((?i4 I_iwf)) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (not (forall ((?z I_iwfl)) (not (= (iwfl_arg_0_14 ?z) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (body!2237 (iwf_arg_0_13 ?i4)) (body!2237_uf_6 (iwf_arg_0_13 ?i4))))) )) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (elze!2246 (iwf_arg_0_13 ?i4)) (elze!2246_uf_4 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (then!2245 (iwf_arg_0_13 ?i4)) (then!2245_uf_5 (iwf_arg_0_13 ?i4))))) ))) (ite (is-While (iwf_arg_0_13 ?i4)) true (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (body!2242 (iwf_arg_0_13 ?i4)) (body!2242_uf_1 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (step!2241 (iwf_arg_0_13 ?i4)) (step!2241_uf_2 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (init!2239 (iwf_arg_0_13 ?i4)) (init!2239_uf_3 (iwf_arg_0_13 ?i4))))) ))) true)))) )
+(is-IfTE s)
+(iwf s) 
+(not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) s)) ))
+(ite (is-IfTE s) (= termITE_17 (then!2245 s)) (= termITE_17 (then!2245_uf_5 s)))
+(ite (is-IfTE s) (= termITE_18 (then!2245 s)) (= termITE_18 (then!2245_uf_5 s)))
+(=> (and (iwf termITE_17) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_18)) ))) (and (= (ewl termITE_17) termITE_17) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_18)) ))))
+(ite (is-IfTE s) (= termITE_19 (elze!2246 s)) (= termITE_19 (elze!2246_uf_4 s)))
+(ite (is-IfTE s) (= termITE_20 (elze!2246 s)) (= termITE_20 (elze!2246_uf_4 s)))
+(=> (and (iwf termITE_19) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_20)) ))) (and (= (ewl termITE_19) termITE_19) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_20)) ))))
+(not (= (ewl s) s))
+(not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) s)) ))
+
+
+)
+)
+(check-sat)
diff --git a/test/regress/regress0/fmf/with-ind-104-core.smt2 b/test/regress/regress0/fmf/with-ind-104-core.smt2
new file mode 100755
index 000000000..a2e3a9ed0
--- /dev/null
+++ b/test/regress/regress0/fmf/with-ind-104-core.smt2
@@ -0,0 +1,33 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Nat!2409 (succ!2410 (pred!2411 Nat!2409)) (zero!2412))
+))
+(declare-datatypes () ((Lst!2413 (cons!2414 (head!2415 Nat!2409) (tail!2416 Lst!2413)) (nil!2417))
+))
+(declare-fun error_value!2418 () Nat!2409)
+(declare-fun plus!237 (Nat!2409 Nat!2409) Nat!2409)
+(declare-fun error_value!2419 () Nat!2409)
+(declare-fun count!263 (Nat!2409 Lst!2413) Nat!2409)
+(declare-fun pred!2411_uf_1 (Nat!2409) Nat!2409)
+(declare-fun tail!2416_uf_2 (Lst!2413) Lst!2413)
+(declare-fun head!2415_uf_3 (Lst!2413) Nat!2409)
+(declare-sort I_plus!237 0)
+(set-info :notes "plus!237_arg_0_4 is op created during fun def fmf")
+(declare-fun plus!237_arg_0_4 (I_plus!237) Nat!2409)
+(set-info :notes "plus!237_arg_1_5 is op created during fun def fmf")
+(declare-fun plus!237_arg_1_5 (I_plus!237) Nat!2409)
+(declare-sort I_count!263 0)
+(set-info :notes "count!263_arg_0_6 is op created during fun def fmf")
+(declare-fun count!263_arg_0_6 (I_count!263) Nat!2409)
+(set-info :notes "count!263_arg_1_7 is op created during fun def fmf")
+(declare-fun count!263_arg_1_7 (I_count!263) Lst!2413)
+(assert
+(and
+(not (forall ((h!413 Nat!2409) (BOUND_VARIABLE_663 I_plus!237) (BOUND_VARIABLE_671 I_count!263) (BOUND_VARIABLE_679 I_count!263) (BOUND_VARIABLE_687 I_count!263) (BOUND_VARIABLE_695 I_plus!237) (BOUND_VARIABLE_703 I_count!263) (BOUND_VARIABLE_711 I_count!263) (BOUND_VARIABLE_719 I_count!263)) (or (not (= (plus!237 (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) (= (plus!237 (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_679) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_687) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_687) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_703) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_703) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_711) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_711) (count!263_arg_1_7 BOUND_VARIABLE_679))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_719) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_719) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) ))
+(forall ((?j I_plus!237)) (= (plus!237 (plus!237_arg_0_4 ?j) (plus!237_arg_1_5 ?j)) (ite (is-zero!2412 (plus!237_arg_0_4 ?j)) (plus!237_arg_1_5 ?j) (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (succ!2410 (plus!237 (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (pred!2411 (plus!237_arg_0_4 ?j)) (pred!2411_uf_1 (plus!237_arg_0_4 ?j))) (plus!237_arg_1_5 ?j))) error_value!2418))) )
+(forall ((?i I_plus!237)) (ite (is-zero!2412 (plus!237_arg_0_4 ?i)) true (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (not (forall ((?z I_plus!237)) (or (not (= (plus!237_arg_0_4 ?z) (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (pred!2411 (plus!237_arg_0_4 ?i)) (pred!2411_uf_1 (plus!237_arg_0_4 ?i))))) (not (= (plus!237_arg_1_5 ?z) (plus!237_arg_1_5 ?i)))) )) true)) )
+(forall ((?i I_count!263)) (= (count!263 (count!263_arg_0_6 ?i) (count!263_arg_1_7 ?i)) (ite (is-nil!2417 (count!263_arg_1_7 ?i)) zero!2412 (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (ite (= (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (head!2415 (count!263_arg_1_7 ?i)) (head!2415_uf_3 (count!263_arg_1_7 ?i)))) (succ!2410 (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) error_value!2419))) )
+(forall ((?j I_count!263)) (ite (is-nil!2417 (count!263_arg_1_7 ?j)) true (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (ite (= (count!263_arg_0_6 ?j) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (head!2415 (count!263_arg_1_7 ?j)) (head!2415_uf_3 (count!263_arg_1_7 ?j)))) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) )) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) ))) true)) )
+)
+)
+(check-sat)
\ No newline at end of file