diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-24 16:56:23 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-24 16:56:41 -0500 |
| commit | 21ac21a2ff3ba3eeac4deabf0c4b79ca4cc8df77 (patch) | |
| tree | ec0f4edcec8ed1c89db9c917a0136b5199021696 /test/regress/regress0/fmf | |
| parent | bcfe5eed9c79e7bd3c32b5ce8e96a54bcff4099f (diff) | |
Fixes and simplifications for fmf mbqi.
Diffstat (limited to 'test/regress/regress0/fmf')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/alg202+1.smt2 | 17 |
2 files changed, 19 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 0c13961cc..a91499a6c 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -71,7 +71,8 @@ TESTS = \ bug782.smt2 \ quant_real_univ.cvc \ constr-ground-to.smt2 \ - bug-041417-set-options.cvc + bug-041417-set-options.cvc \ + alg202+1.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/alg202+1.smt2 b/test/regress/regress0/fmf/alg202+1.smt2 new file mode 100644 index 000000000..ff3460636 --- /dev/null +++ b/test/regress/regress0/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) |