diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/bug_743.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/bug_743.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress1/quantifiers/bug_743.smt2 b/test/regress/regress1/quantifiers/bug_743.smt2 index 8b20cf5ca..e2fff8018 100644 --- a/test/regress/regress1/quantifiers/bug_743.smt2 +++ b/test/regress/regress1/quantifiers/bug_743.smt2 @@ -253,13 +253,13 @@ i))) (+ (- i a_last) (- b_first 1)))))) :pattern ((select (concat1 a a_first a_last b b_first b_last) i)) ))))) -(declare-fun singleton (natural Int) (Array Int natural)) +(declare-fun set.singleton (natural Int) (Array Int natural)) ;; singleton_def (assert (forall ((v natural)) (forall ((i Int)) - (! (= (select (singleton v i) i) v) :pattern ((select (singleton v i) + (! (= (select (set.singleton v i) i) v) :pattern ((select (set.singleton v i) i)) )))) (declare-fun compare ((Array Int natural) Int Int (Array Int natural) Int |