diff options
| -rw-r--r-- | test/regress/regress1/fmf/fmf-strange-bounds.smt2 | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 index 7812c2431..bdbca4bd0 100644 --- a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 +++ b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound +; COMMAND-LINE: --fmf-bound --finite-model-find ; EXPECT: sat (set-logic ALL) (set-info :status sat) @@ -23,6 +23,12 @@ (=> (and (<= 0 y) (<= y (h z))) (P x y z)))))) +(assert (forall ((x Int) (y Int) (z U)) (=> +(or (= x 5) (= x 6)) +(=> (and (<= 0 y) (<= y x)) +(P x y z))))) + + (declare-fun Q (U Int) Bool) (declare-const a U) |