diff options
Diffstat (limited to 'test/regress/regress1/fmf/alg202+1.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/alg202+1.smt2 | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/alg202+1.smt2 b/test/regress/regress1/fmf/alg202+1.smt2 new file mode 100644 index 000000000..ff3460636 --- /dev/null +++ b/test/regress/regress1/fmf/alg202+1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-fun sorti1 ($$unsorted) Bool) +(declare-fun op1 ($$unsorted $$unsorted) $$unsorted) +(declare-fun sorti2 ($$unsorted) Bool) +(declare-fun op2 ($$unsorted $$unsorted) $$unsorted) +(declare-fun h ($$unsorted) $$unsorted) +(declare-fun j ($$unsorted) $$unsorted) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_345 $$unsorted)) (or (not (sorti1 U)) (not (sorti1 BOUND_VARIABLE_345)) (sorti1 (op1 U BOUND_VARIABLE_345))) )) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_364 $$unsorted)) (or (not (sorti2 U)) (not (sorti2 BOUND_VARIABLE_364)) (sorti2 (op2 U BOUND_VARIABLE_364))) )) +(assert (forall ((U $$unsorted)) (or (not (sorti1 U)) (= U (op1 U U))) )) +(assert (not (forall ((U $$unsorted)) (or (not (sorti2 U)) (= U (op2 U U))) ))) +(assert (not (=> (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) )) (not (and (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) )))))) +(assert (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) ) (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) ))) +(check-sat) |