diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
| commit | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (patch) | |
| tree | 57cee5cddf68999e20553ee9746f4a83183e8b99 /test/regress/regress0 | |
| parent | 576d50ac7c13233a589771401537b587eb36361e (diff) | |
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/double-pattern.smt2 | 6 |
2 files changed, 8 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f0c9b5a33..784eaf677 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -76,7 +76,8 @@ TESTS = \ subtype-param.smt2 \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ - florian-case-ax.smt2 + florian-case-ax.smt2 \ + double-pattern.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2 new file mode 100644 index 000000000..4ce21d446 --- /dev/null +++ b/test/regress/regress0/quantifiers/double-pattern.smt2 @@ -0,0 +1,6 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x))))) +(assert (not (P 0))) +(check-sat) |