Refactor regressions (#1581)

1 files changed, 87 insertions, 0 deletions

diff --git a/test/regress/regress1/quantifiers/z3.620661-no-fv-trigger.smt2 b/test/regress/regress1/quantifiers/z3.620661-no-fv-trigger.smt2
new file mode 100644
index 000000000..aad2a4691
--- /dev/null
+++ b/test/regress/regress1/quantifiers/z3.620661-no-fv-trigger.smt2
@@ -0,0 +1,87 @@
+(set-logic AUFNIRA)
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-sort S2 0)
+(declare-sort S3 0)
+(declare-sort S4 0)
+(declare-sort S5 0)
+(declare-sort S6 0)
+(declare-sort S7 0)
+(declare-sort S8 0)
+(declare-sort S9 0)
+(declare-sort S10 0)
+(declare-sort S11 0)
+(declare-sort S12 0)
+(declare-sort S13 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (S2 Real) Real)
+(declare-fun f4 (S3 Real) S2)
+(declare-fun f5 () S3)
+(declare-fun f6 (S4 Int) Int)
+(declare-fun f7 (S5 Int) S4)
+(declare-fun f8 () S5)
+(declare-fun f9 () S2)
+(declare-fun f10 () Real)
+(declare-fun f11 () Real)
+(declare-fun f12 () S2)
+(declare-fun f13 (S7 S6) Real)
+(declare-fun f14 () S7)
+(declare-fun f15 () S2)
+(declare-fun f16 () S2)
+(declare-fun f17 (S8 Int) S6)
+(declare-fun f18 () S8)
+(declare-fun f19 (S9 S6) Int)
+(declare-fun f20 () S9)
+(declare-fun f21 (S10 Real) S7)
+(declare-fun f22 () S10)
+(declare-fun f23 () S2)
+(declare-fun f24 (S11 S6) S6)
+(declare-fun f25 (S12 S6) S11)
+(declare-fun f26 () S12)
+(declare-fun f27 () S12)
+(declare-fun f28 (S13 Int) S9)
+(declare-fun f29 () S13)
+(declare-fun f30 () S2)
+(declare-fun f31 () S4)
+(assert (not (= f1 f2)))
+(assert (forall ((?v0 Real) (?v1 Real)) (= (f3 (f4 f5 ?v0) ?v1) (* ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (f6 (f7 f8 ?v0) ?v1) (* ?v0 ?v1))))
+(assert (not (= (f3 f9 (- f10 f11)) (- (f3 f9 f10)))))
+(assert (= (f3 f9 f11) 0.0))
+(assert (forall ((?v0 Real)) (= (f3 f9 (+ f11 ?v0)) (- (f3 f9 ?v0)))))
+(assert (= (f3 f9 (/ f11 2.0)) 1.0))
+(assert (= (f3 f9 (/ f11 6.0)) (/ 1.0 2.0)))
+(assert (= (f3 f9 (* 2.0 f11)) 0.0))
+(assert (= (f3 f9 (* (/ 3.0 2.0) f11)) (- 1.0)))
+(assert (let ((?v_0 2.0)) (<= (/ f11 ?v_0) ?v_0)))
+(assert (let ((?v_0 2.0)) (< (/ f11 ?v_0) ?v_0)))
+(assert (< (- (* 2.0 f11)) f11))
+(assert (< (- (/ f11 2.0)) 0.0))
+(assert (<= 2.0 f11))
+(assert (<= 0.0 (/ f11 2.0)))
+(assert (< 0.0 (/ f11 2.0)))
+(assert (< f11 4.0))
+(assert (<= 0.0 f11))
+(assert (< 0.0 f11))
+(assert (let ((?v_0 2.0)) (not (= (/ f11 ?v_0) ?v_0))))
+(assert (not (= (/ f11 2.0) 0.0)))
+(assert (not (< f11 0.0)))
+(assert (not (= f11 0.0)))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (= (f13 f14 ?v0) (f13 f14 ?v1)) (= ?v0 ?v1))))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (< (f13 f14 ?v0) (f13 f14 ?v1)) (< (f19 f20 ?v0) (f19 f20 ?v1)))))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (<= (f13 f14 ?v0) (f13 f14 ?v1)) (<= (f19 f20 ?v0) (f19 f20 ?v1)))))
+(assert (forall ((?v0 S6) (?v1 S6)) (let ((?v_0 (f19 f20 ?v1)) (?v_1 (f19 f20 ?v0))) (=> (<= ?v_1 ?v_0) (= (f13 f14 (f17 f18 (- ?v_0 ?v_1))) (- (f13 f14 ?v1) (f13 f14 ?v0)))))))
+(assert (forall ((?v0 Real) (?v1 Real)) (exists ((?v2 Real) (?v3 Real)) (and (= ?v0 (* ?v2 (f3 f15 ?v3))) (= ?v1 (* ?v2 (f3 f9 ?v3)))))))
+(assert (< 1.0 (f3 f16 2.0)))
+(assert (< 0.0 (f3 f16 2.0)))
+(assert (<= 0.0 (f3 f16 2.0)))
+(assert (forall ((?v0 Real) (?v1 Real)) (<= 0.0 (f3 f16 (+ (* ?v0 ?v0) (* ?v1 ?v1))))))
+(assert (forall ((?v0 Real) (?v1 Real)) (=> (<= ?v0 ?v1) (<= (f3 f16 ?v0) (f3 f16 ?v1)))))
+(assert (forall ((?v0 Real) (?v1 Real)) (=> (< ?v0 ?v1) (< (f3 f16 ?v0) (f3 f16 ?v1)))))
+(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (=> (= (f3 f16 ?v0) ?v_0) (= ?v0 ?v_0))))))
+(assert (forall ((?v0 Real)) (=> (< 0.0 ?v0) (< (/ ?v0 (f3 f16 2.0)) ?v0))))
+(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0))))))
+(assert (forall ((?v0 Real)) (let ((?v_0 1.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0))))))
+(check-sat)
+(exit)