Fix fmf benchmark (#4193)

Fixes regress1.

This benchmark is too delicate in the current state.

diff --git a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 b/test/regress/regress1/fmf/fmf-strange-bounds.smt2
index bdbca4bd0117c6a9923761919b90d72dce5da6dd..20738245c3cf4f27ba58a1bca9f0b2cf377d4d6a 100644 (file)
--- a/test/regress/regress1/fmf/fmf-strange-bounds.smt2
+++ b/test/regress/regress1/fmf/fmf-strange-bounds.smt2
@@ -17,11 +17,10 @@
 (assert (>= (h (g 77)) 2))
 (assert (not (= (g 77) (f 77))))
 
-(assert (forall ((x Int) (y Int) (z U)) (=> 
+(assert (forall ((x Int) (z U)) (=> 
 (or (= z (f x)) (= z (g x)))
 (=> (member x S)
-(=> (and (<= 0 y) (<= y (h z)))
-(P x y z))))))
+(P x 0 z)))))
 
 (assert (forall ((x Int) (y Int) (z U)) (=>
 (or (= x 5) (= x 6))