diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/macros-real-arg.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/macros-real-arg.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 index 675c96d68..edacdbe37 100644 --- a/test/regress/regress0/quantifiers/macros-real-arg.smt2 +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -6,6 +6,6 @@ (assert (forall ((x Int)) (P x))) (declare-fun k () Real) (declare-fun k2 () Int) -(assert (or (not (P k)) (not (P k2)))) +(assert (or (not (P (to_int k))) (not (P k2)))) (assert (= k 0)) (check-sat) |