diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-10 08:12:34 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-10 08:12:34 +0200 |
| commit | d5b0866bd2a2551143caf591d453993ab5a48840 (patch) | |
| tree | 71d9bf61a8134be3ca13596ab0d8f278a2021eb9 /test/regress/regress0/sets/Makefile.am | |
| parent | 8a68cca2f9cf76b42187c39d09a4a40bd19622c1 (diff) | |
Ensure that expand definitions is called on all non-variable expressi… (#1070)
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
Diffstat (limited to 'test/regress/regress0/sets/Makefile.am')
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index c8e416a42..de2170768 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ sets-poly-nonint.smt2 \ int-real-univ.smt2 \ int-real-univ-unsat.smt2 \ - sets-tuple-poly.cvc + sets-tuple-poly.cvc \ + arjun-set-univ.cvc \ + univ-set-uf-elim.smt2 EXTRA_DIST = $(TESTS) |