diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-17 18:01:10 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
| commit | c8b948c37364104bf5f9ca5eca83120247b693a4 (patch) | |
| tree | a4fba0d7ba7b8a1f93ff44878414fdda2e9ed941 /test/regress | |
| parent | dead33e1660596c75f2bfc5ee86ed39600a92a45 (diff) | |
Fix for registration issues of term appearing in a shared lemma
(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/sets/sets-testlemma-ints.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 index c8277be71..9dd257401 100644 --- a/test/regress/regress0/sets/sets-testlemma-ints.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -3,5 +3,5 @@ (set-info :status sat) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x y)) +(assert (not (= x y))) (check-sat) |