diff options
Diffstat (limited to 'test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 new file mode 100644 index 000000000..619779c78 --- /dev/null +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 @@ -0,0 +1,90 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-option :incremental false) +(set-info :status sat) +(set-logic AUFLIA) +(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-sort S14 0) +(declare-sort S15 0) +(declare-sort S16 0) +(declare-sort S17 0) +(declare-sort S18 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (S2 S3) S4) +(declare-fun f4 () S2) +(declare-fun f5 () S3) +(declare-fun f6 () S4) +(declare-fun f7 (S3 S5) S1) +(declare-fun f8 (S6) S5) +(declare-fun f9 () S6) +(declare-fun f10 (S7 S6) S6) +(declare-fun f11 () S7) +(declare-fun f12 (S8 S4) S4) +(declare-fun f13 () S8) +(declare-fun f14 (S10 S3) S3) +(declare-fun f15 (S11 S9) S10) +(declare-fun f16 (S12 S4) S11) +(declare-fun f17 () S12) +(declare-fun f18 (S4 S13) S1) +(declare-fun f19 () S13) +(declare-fun f20 (S4) S1) +(declare-fun f21 () S2) +(declare-fun f22 () S10) +(declare-fun f23 (S3 S9) S1) +(declare-fun f24 (S14 S9) S9) +(declare-fun f25 (S15 S4) S14) +(declare-fun f26 () S15) +(declare-fun f27 () S13) +(declare-fun f28 () S8) +(declare-fun f29 (S16 S9) S3) +(declare-fun f30 (S17 S4) S16) +(declare-fun f31 (S18 S4) S17) +(declare-fun f32 () S18) +(declare-fun f33 () S18) +(declare-fun f34 (S4 S4) S1) +(assert (not (= f1 f2))) +(assert (not (not (= (f3 f4 f5) f6)))) +(assert (forall ((?v0 S3)) (=> (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) )) +(assert (= (f7 f5 (f8 (f10 f11 f9))) f1)) +(assert (forall ((?v0 S4)) (= (= f6 ?v0) (= ?v0 f6)) )) +(assert (= (f12 f13 f6) f6)) +(assert (forall ((?v0 S4)) (= (= f6 (f12 f13 ?v0)) (= ?v0 f6)) )) +(assert (forall ((?v0 S4)) (= (= (f12 f13 ?v0) f6) (= ?v0 f6)) )) +(assert (forall ((?v0 S4) (?v1 S9) (?v2 S3)) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) )) +(assert (= (f18 f6 f19) f1)) +(assert (= (f20 f6) f1)) +(assert (forall ((?v0 S4)) (= (= (f20 ?v0) f1) (= ?v0 f6)) )) +(assert (forall ((?v0 S3)) (=> (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) )) +(assert (forall ((?v0 S3)) (=> (not (not (= (f3 f21 ?v0) f6))) (=> (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) )) +(assert (forall ((?v0 S4) (?v1 S4)) (= (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) )) +(assert (forall ((?v0 S6) (?v1 S9)) (=> (forall ((?v2 S3)) (=> (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6))) ) (= (exists ((?v2 S4)) (forall ((?v3 S3)) (=> (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)) ) ) (exists ((?v2 S4)) (forall ((?v3 S3)) (=> (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)) ) ))) )) +(assert (forall ((?v0 S4)) (= (f18 (f12 f13 ?v0) f27) f1) )) +(assert (= (f12 f28 f6) f6)) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9)) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9)) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) )) +(assert (= (f18 f6 f27) f1)) +(assert (forall ((?v0 S3) (?v1 S4) (?v2 S9)) (=> (not (not (= (f3 f21 ?v0) f6))) (= (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) )) +(assert (forall ((?v0 S4)) (= (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) )) +(assert (forall ((?v0 S4)) (= (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (not (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5))) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (not (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5))) )) +(assert (forall ((?v0 S4)) (= (f34 ?v0 ?v0) f1) )) +(assert (forall ((?v0 S4) (?v1 S4)) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (= (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (= (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )) +(assert (forall ((?v0 S4) (?v1 S4) (?v2 S4)) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) )) +(assert (forall ((?v0 S4) (?v1 S4)) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) )) +(check-sat-assuming ( true )) |