test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2

   1 ; COMMAND-LINE: --finite-model-find -q
   2 ; EXPECT: sat
   3 (set-option :incremental false)
   4 (set-info :status sat)
   5 (set-logic AUFLIA)
   6 (declare-sort S1 0)
   7 (declare-sort S2 0)
   8 (declare-sort S3 0)
   9 (declare-sort S4 0)
  10 (declare-sort S5 0)
  11 (declare-sort S6 0)
  12 (declare-sort S7 0)
  13 (declare-sort S8 0)
  14 (declare-sort S9 0)
  15 (declare-sort S10 0)
  16 (declare-sort S11 0)
  17 (declare-fun f1 () S1)
  18 (declare-fun f2 () S1)
  19 (declare-fun f3 (S3 S2) S1)
  20 (declare-fun f4 (S4 S2) S3)
  21 (declare-fun f5 () S4)
  22 (declare-fun f6 (S5 S5) S1)
  23 (declare-fun f7 () S5)
  24 (declare-fun f8 (S6 S5) S5)
  25 (declare-fun f9 (S7) S6)
  26 (declare-fun f10 (S8 S4) S7)
  27 (declare-fun f11 (S9 S10) S8)
  28 (declare-fun f12 (S11 S4) S9)
  29 (declare-fun f13 () S11)
  30 (declare-fun f14 () S4)
  31 (declare-fun f15 () S10)
  32 (declare-fun f16 () S4)
  33 (declare-fun f17 (S10) S4)
  34 (declare-fun f18 (S5 S5) S1)
  35 (assert (not (= f1 f2)))
  36 (assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
  37 (assert (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)))
  38 (assert (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1))
  39 (assert (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1))
  40 (assert (forall ((?v0 S5)) (= (f6 ?v0 f7) f1) ))
  41 (assert (forall ((?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4)) (= (= (f10 (f11 (f12 f13 ?v0) ?v1) ?v2) (f10 (f11 (f12 f13 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ))
  42 (assert (forall ((?v0 S5) (?v1 S5)) (=> (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) ))
  43 (assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (=> (= (f6 ?v0 ?v1) f1) (=> (= (f6 ?v2 ?v0) f1) (= (f6 ?v2 ?v1) f1))) ))
  44 (assert (forall ((?v0 S5) (?v1 S7) (?v2 S5)) (let ((_let_0 (f9 ?v1))) (=> (= (f6 ?v0 (f8 _let_0 f7)) f1) (=> (= (f6 ?v0 ?v2) f1) (= (f6 ?v0 (f8 _let_0 ?v2)) f1)))) ))
  45 (assert (forall ((?v0 S5) (?v1 S7) (?v2 S5)) (let ((_let_0 (f9 ?v1))) (=> (= (f6 ?v0 (f8 _let_0 ?v2)) f1) (and (= (f6 ?v0 (f8 _let_0 f7)) f1) (= (f6 ?v0 ?v2) f1)))) ))
  46 (assert (forall ((?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4)) (let ((_let_0 (f11 (f12 f13 ?v1) ?v2))) (=> (= (f6 ?v0 (f8 (f9 (f10 _let_0 ?v3)) f7)) f1) (=> (forall ((?v5 S2) (?v6 S2)) (=> (= (f3 (f4 ?v3 ?v5) ?v6) f1) (= (f3 (f4 ?v4 ?v5) ?v6) f1)) ) (= (f6 ?v0 (f8 (f9 (f10 _let_0 ?v4)) f7)) f1)))) ))
  47 (assert (forall ((?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4)) (=> (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (=> (forall ((?v5 S2) (?v6 S2)) (=> (= (f3 (f4 ?v4 ?v5) ?v6) f1) (= (f3 (f4 ?v1 ?v5) ?v6) f1)) ) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v4) ?v2) ?v3)) f7)) f1))) ))
  48 (check-sat-assuming ( true ))