diff options
Diffstat (limited to 'test/regress/regress0/arrays')
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/arrays/constarr3.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/arrays/constarr3.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress0/arrays/parsing_ringer.cvc | 94 |
4 files changed, 0 insertions, 125 deletions
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 17cfa3fd4..bdc7352f5 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -44,11 +44,8 @@ TESTS = \ bug272.minimized.smt \ constarr.smt2 \ constarr2.smt2 \ - constarr3.smt2 \ constarr.cvc \ constarr2.cvc \ - constarr3.cvc \ - parsing_ringer.cvc \ bug637.delta.smt2 \ bool-array.smt2 diff --git a/test/regress/regress0/arrays/constarr3.cvc b/test/regress/regress0/arrays/constarr3.cvc deleted file mode 100644 index bf5cf961c..000000000 --- a/test/regress/regress0/arrays/constarr3.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXIT: 1 -% EXPECT: Array theory solver does not yet support write-chains connecting two different constant arrays -% should be unsat -all1, all2 : ARRAY INT OF INT; -aa, bb : ARRAY INT OF INT; -a, i : INT; -ASSERT all1 = ARRAY(INT OF INT) : 1; -ASSERT aa = all1 WITH [i] := 0; -ASSERT all2 = ARRAY(INT OF INT) : 2; -ASSERT bb = all2 WITH [i] := 0; -ASSERT aa = bb; -CHECKSAT; diff --git a/test/regress/regress0/arrays/constarr3.smt2 b/test/regress/regress0/arrays/constarr3.smt2 deleted file mode 100644 index d514fff70..000000000 --- a/test/regress/regress0/arrays/constarr3.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; EXIT: 1 -; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") -(set-logic QF_ALIA) -(set-info :status unsat) -(declare-const all1 (Array Int Int)) -(declare-const all2 (Array Int Int)) -(declare-const aa (Array Int Int)) -(declare-const bb (Array Int Int)) -(declare-const a Int) -(declare-const i Int) -(assert (= all1 ((as const (Array Int Int)) 1))) -(assert (= aa (store all1 i 0))) -(assert (= all2 ((as const (Array Int Int)) 2))) -(assert (= bb (store all2 i 0))) -(assert (= aa bb)) -(check-sat) diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc deleted file mode 100644 index 2c2018ecd..000000000 --- a/test/regress/regress0/arrays/parsing_ringer.cvc +++ /dev/null @@ -1,94 +0,0 @@ -% Test for presentiation language parsing, some edge cases with cascading -% store terms. Intended to put this part of the parser "through the ringer," -% hence the name. - -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: sat -% EXPECT: unsat -% EXPECT: unsat -% EXPECT: sat - -PUSH; - -x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT; - -% multidimensional arrays -ASSERT x[0][0][0] = 0; %% select -ASSERT y = x WITH [0][0][1] := 1; %% partial store - -CHECKSAT; - -% mixed stores: records of arrays of tuples, oh my -z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #]; - -arr1 : ARRAY INT OF [# x:INT #]; -arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ]; - -ASSERT arr1[0].x = 0; -ASSERT arr2.0[0] = 1; -ASSERT arr2.1[0] = 5; - -ASSERT z.y.1[1] /= 1; -ASSERT (# x:=arr1, y:=arr2 #) = z; - -CHECKSAT; - -ASSERT z.x[0].x /= z.y.0[5]; - -CHECKSAT; - -ASSERT z.y.0[1] = z.x[5].x; - -CHECKSAT; - -ASSERT z.y.0[5] = z.x[-2].x; - -CHECKSAT; - -POP; - -a : ARRAY INT OF ARRAY INT OF INT; -b : ARRAY INT OF INT; - -% ambiguity in presentation language, comma needs to bind to innermost WITH -% causes type error if the [2]:=2 at the end is attached to the wrong WITH -ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2; - -CHECKSAT; - -RESET; - -% more mixed stores, this time with constant arrays -z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #]; - -ASSERT z.y.1[1] /= 1; -ASSERT (# x:=ARRAY(INT OF [# x:INT #]):(# x:=0 #), y:=(ARRAY(INT OF INT):1, ARRAY(INT OF INT):5) #) = z; - -CHECKSAT; - -ASSERT z.x[0].x /= z.y.0[5]; - -CHECKSAT; - -ASSERT z.y.0[1] = z.x[5].x; - -CHECKSAT; - -ASSERT z.y.0[5] = z.x[-2].x; - -CHECKSAT; - -RESET; - -a : ARRAY INT OF INT; - -ASSERT a = a WITH [0]:=0, [1]:=1; - -CHECKSAT; |