From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 31 Mar 2020 20:25:01 +0000 (-0500)
Subject: Fix fmf benchmark (#4193)
X-Git-Tag: cvc5-1.0.0~3418
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bded1a268b0ca9959ca1223dd04de8db535cc99a;p=cvc5.git

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 bdbca4bd0..20738245c 100644
--- 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))