update golds

LeventErkok · Sep 17, 2024 · fbdd4ce · fbdd4ce
1 parent 0d06440
commit fbdd4ce
Show file tree

Hide file tree

Showing 299 changed files with 773 additions and 1,578 deletions.
diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x0010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x00000010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x0000000000000010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word8.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word8.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x10 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00) s0))
 [GOOD] (assert (= (table0 #x01) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x0020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x00000020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x0000000000000020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word8.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word8.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x20 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00) s0))
 [GOOD] (assert (= (table0 #x01) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 64))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -111,8 +110,6 @@
 [GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_left 63) s0))
 [GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x0040 s3) s91 (table0 s3)))
 [GOOD] (define-fun s93 () Bool (= s28 s92))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s17))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 64))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -111,8 +110,6 @@
 [GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_left 63) s0))
 [GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x00000040 s3) s91 (table0 s3)))
 [GOOD] (define-fun s93 () Bool (= s28 s92))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s17))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 64))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -111,8 +110,6 @@
 [GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_left 63) s0))
 [GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x0000000000000040 s3) s91 (table0 s3)))
 [GOOD] (define-fun s93 () Bool (= s28 s92))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s17))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word8.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word8.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 64))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -111,8 +110,6 @@
 [GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_left 63) s0))
 [GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x40 s3) s91 (table0 s3)))
 [GOOD] (define-fun s93 () Bool (= s28 s92))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00) s0))
 [GOOD] (assert (= (table0 #x01) s17))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 8))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -43,8 +42,6 @@
 [GOOD] (define-fun s22 () (_ BitVec 8) ((_ rotate_left 7) s0))
 [GOOD] (define-fun s24 () (_ BitVec 8) (ite (bvule #x0008 s3) s23 (table0 s3)))
 [GOOD] (define-fun s25 () Bool (= s16 s24))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s11))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 8))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -43,8 +42,6 @@
 [GOOD] (define-fun s22 () (_ BitVec 8) ((_ rotate_left 7) s0))
 [GOOD] (define-fun s24 () (_ BitVec 8) (ite (bvule #x00000008 s3) s23 (table0 s3)))
 [GOOD] (define-fun s25 () Bool (= s16 s24))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s11))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 8))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -43,8 +42,6 @@
 [GOOD] (define-fun s22 () (_ BitVec 8) ((_ rotate_left 7) s0))
 [GOOD] (define-fun s24 () (_ BitVec 8) (ite (bvule #x0000000000000008 s3) s23 (table0 s3)))
 [GOOD] (define-fun s25 () Bool (= s16 s24))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s11))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word8.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word8.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -43,8 +42,6 @@
 [GOOD] (define-fun s22 () (_ BitVec 8) ((_ rotate_left 7) s0))
 [GOOD] (define-fun s24 () (_ BitVec 8) (ite (bvule #x08 s3) s23 (table0 s3)))
 [GOOD] (define-fun s25 () Bool (= s16 s24))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00) s0))
 [GOOD] (assert (= (table0 #x01) s11))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x0010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x00000010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x0000000000000010 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word8.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word8.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 16))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -55,8 +54,6 @@
 [GOOD] (define-fun s34 () (_ BitVec 16) ((_ rotate_left 15) s0))
 [GOOD] (define-fun s36 () (_ BitVec 16) (ite (bvule #x10 s3) s35 (table0 s3)))
 [GOOD] (define-fun s37 () Bool (= s20 s36))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00) s0))
 [GOOD] (assert (= (table0 #x01) s13))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word16.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word16.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x0020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000) s0))
 [GOOD] (assert (= (table0 #x0001) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word32.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word32.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 32)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x00000020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x00000000) s0))
 [GOOD] (assert (= (table0 #x00000001) s15))

diff --git a/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word64.gold b/SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word64.gold
@@ -18,7 +18,6 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 32))
-[GOOD] ; --- arrays ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
@@ -75,8 +74,6 @@
 [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0))
 [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x0000000000000020 s3) s55 (table0 s3)))
 [GOOD] (define-fun s57 () Bool (= s24 s56))
-[GOOD] ; --- arrayDelayeds ---
-[GOOD] ; --- arraySetups ---
 [GOOD] ; --- delayedEqualities ---
 [GOOD] (assert (= (table0 #x0000000000000000) s0))
 [GOOD] (assert (= (table0 #x0000000000000001) s15))