summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/fuzz31811.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/fuzz31811.smt2')
-rw-r--r--test/regress/regress0/sets/fuzz31811.smt220
1 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2
index 799dda0e2..5e7c032ea 100644
--- a/test/regress/regress0/sets/fuzz31811.smt2
+++ b/test/regress/regress0/sets/fuzz31811.smt2
@@ -9,7 +9,7 @@
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
(define-sort Element () Int)
(declare-fun f0 ( Int Int Int) Int)
(declare-fun f1 ( (Set Element) (Set Element)) (Set Element))
@@ -26,27 +26,27 @@
(let ((e8 (* e6 (- e5))))
(let ((e9 (ite (p0 e7 v0 e6) 1 0)))
(let ((e10 (f0 v0 e8 e8)))
-(let ((e11 (ite (p1 v1) (setenum 1) (setenum 0))))
+(let ((e11 (ite (p1 v1) (singleton 1) (singleton 0))))
(let ((e12 (union v3 v3)))
(let ((e13 (intersection v3 v1)))
-(let ((e14 (ite (p1 v3) (setenum 1) (setenum 0))))
+(let ((e14 (ite (p1 v3) (singleton 1) (singleton 0))))
(let ((e15 (intersection v2 e14)))
-(let ((e16 (ite (p1 e11) (setenum 1) (setenum 0))))
-(let ((e17 (ite (p1 v4) (setenum 1) (setenum 0))))
+(let ((e16 (ite (p1 e11) (singleton 1) (singleton 0))))
+(let ((e17 (ite (p1 v4) (singleton 1) (singleton 0))))
(let ((e18 (union e15 v2)))
-(let ((e19 (ite (p1 e16) (setenum 1) (setenum 0))))
+(let ((e19 (ite (p1 e16) (singleton 1) (singleton 0))))
(let ((e20 (intersection e18 v3)))
(let ((e21 (setminus v4 e12)))
(let ((e22 (union v3 v2)))
(let ((e23 (setminus e12 v4)))
(let ((e24 (setminus v3 e16)))
(let ((e25 (intersection e19 e20)))
-(let ((e26 (ite (p1 e15) (setenum 1) (setenum 0))))
+(let ((e26 (ite (p1 e15) (singleton 1) (singleton 0))))
(let ((e27 (setminus e17 e15)))
(let ((e28 (f1 e23 e12)))
-(let ((e29 (in e10 e16)))
-(let ((e30 (in e10 v1)))
-(let ((e31 (in e7 e19)))
+(let ((e29 (member e10 e16)))
+(let ((e30 (member e10 v1)))
+(let ((e31 (member e7 e19)))
(let ((e32 (f1 e12 e12)))
(let ((e33 (f1 e16 e25)))
(let ((e34 (f1 v1 e27)))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback