diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/macros-real-arg.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/macros-real-arg.smt2 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 index edacdbe37..52eeedae6 100644 --- a/test/regress/regress0/quantifiers/macros-real-arg.smt2 +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -3,7 +3,8 @@ ; this will fail if type rule for APPLY_UF is made strict (set-logic UFLIRA) (declare-fun P (Int) Bool) -(assert (forall ((x Int)) (P x))) +(declare-fun Q (Int) Bool) +(assert (and (forall ((x Int)) (P x)) (forall ((x Int)) (Q x)))) (declare-fun k () Real) (declare-fun k2 () Int) (assert (or (not (P (to_int k))) (not (P k2)))) |