diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /test/regress/regress0/fmf/bounded_sets.smt2 | |
parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) |
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
Diffstat (limited to 'test/regress/regress0/fmf/bounded_sets.smt2')
-rw-r--r-- | test/regress/regress0/fmf/bounded_sets.smt2 | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/bounded_sets.smt2 b/test/regress/regress0/fmf/bounded_sets.smt2 new file mode 100644 index 000000000..b06c3636f --- /dev/null +++ b/test/regress/regress0/fmf/bounded_sets.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun S () (Set Int)) +(declare-fun P (Int) Bool) +(declare-fun a () Int) +(assert (member a S)) +(assert (forall ((y Int)) (=> (member y S) (P y)))) + + +(declare-fun T () (Set Int)) +(declare-fun b () Int) +(assert (member b T)) +(assert (forall ((y Int)) (=> (member y T) (not (P y))))) + +(check-sat) |