diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-11-05 09:25:09 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-11-05 09:25:09 -0800 |
| commit | d5023d2ec57dd741fcec1aaa5da8dedccd90aa02 (patch) | |
| tree | c414cbdfe5c2a8e4643f6907fedde683525a7c6c /test/regress/regress0/quantifiers | |
| parent | 52ee910c128e6bbcf7299a0660511deacadb14f1 (diff) | |
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -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)))) |