about summary refs log tree commit diff homepage
path: root/test/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'test/Expr')
-rw-r--r--test/Expr/Lexer/dg.exp3
-rw-r--r--test/Expr/Parser/ConstantFolding.pc172
-rw-r--r--test/Expr/Parser/MultiByteReads.pc6
-rw-r--r--test/Expr/Parser/Simplify.pc30
-rw-r--r--test/Expr/Parser/dg.exp3
-rw-r--r--test/Expr/dg.exp3
-rw-r--r--test/Expr/print-smt.smt2.good22
7 files changed, 115 insertions, 124 deletions
diff --git a/test/Expr/Lexer/dg.exp b/test/Expr/Lexer/dg.exp
deleted file mode 100644
index 94fc4df8..00000000
--- a/test/Expr/Lexer/dg.exp
+++ /dev/null
@@ -1,3 +0,0 @@
-load_lib llvm.exp
-
-RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]]
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc
index 2c8a4c52..a02920db 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.pc
@@ -2,196 +2,196 @@
 
 array a[64] : w32 -> w8 = symbolic
 
-# RUN: grep -A 2 \"# Query 1$\" %t > %t2
-# RUN: grep \"(query .. false)\" %t2
+# RUN: grep -A 2 "# Query 1$" %t > %t2
+# RUN: grep "(query .. false)" %t2
 (query [] (Not (Ult (w32 0) (w32 1))))
 
 # Check -- 0 + X ==> X
-# RUN: grep -A 2 \"# Query 2$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2
+# RUN: grep -A 2 "# Query 2$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a).)" %t2
 (query [] false [(Add w8 0 (Read w8 0 a))])
-# RUN: grep -A 2 \"# Query 3$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2
+# RUN: grep -A 2 "# Query 3$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a).)" %t2
 (query [] false [(Add w8 (Read w8 0 a) 0)])
 
 # Check -- C_0 + (C_1 + X) ==> (C_0 + C_1) + X
-# RUN: grep -A 2 \"# Query 4$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 4$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2
 (query [] false [(Add w8 10 (Add w8 20 (Read w8 0 a)))])
 
 # Check -- C_0 + (X + C_1) ==> (C_0 + C_1) + X
-# RUN: grep -A 2 \"# Query 5$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 5$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2
 (query [] false [(Add w8 10 (Add w8 (Read w8 0 a) 20))])
 
 # Check -- C_0 + (C_1 - X) ==> (C_0 + C_1) - X
-# RUN: grep -A 2 \"# Query 6$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 30 (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 6$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a)).)" %t2
 (query [] false [(Add w8 10 (Sub w8 20 (Read w8 0 a)))])
 
 # Check -- C_0 + (X - C_1) ==> (C_0 - C_1) + X
-# RUN: grep -A 2 \"# Query 7$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 7$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a)).)" %t2
 (query [] false [(Add w8 10 (Sub w8 (Read w8 0 a) 20))])
 
 # Check -- (X + Y) + Z ==> X + (Y + Z)
-# RUN: grep -A 3 \"# Query 8$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 1 a) (Read w8 2 a)\" %t2
+# RUN: grep -A 3 "# Query 8$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2
+# RUN: grep                          "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2
 (query [] false [(Add w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- (X - Y) + Z ==> X + (Z - Y)
-# RUN: grep -A 3 \"# Query 9$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 2 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 9$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2
+# RUN: grep                          "(Sub w8 (Read w8 2 a) (Read w8 1 a)" %t2
 (query [] false [(Add w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- X + (C + Y) ==> C + (X + Y)
-# RUN: grep -A 3 \"# Query 10$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 10\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 10$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 10" %t2
+# RUN: grep                          "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))])
 
 # Check -- X + (Y + C) ==> C + (X + Y)
-# RUN: grep -A 3 \"# Query 11$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 10\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 11$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 10" %t2
+# RUN: grep                          "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))])
 
 # Check -- X + (C - Y) ==> C + (X - Y)
-# RUN: grep -A 3 \"# Query 12$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 10\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 12$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 10" %t2
+# RUN: grep                          "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))])
 
 # Check -- X + (Y - C) ==> -C + (X + Y)
-# RUN: grep -A 3 \"# Query 13$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 13$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246" %t2
+# RUN: grep                          "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))])
 
 # Check -- C_0 - (C_1 + X) ==> (C_0 - C1) - X
-# RUN: grep -A 2 \"# Query 14$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 10 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 14$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 20 (Add w8 10 (Read w8 0 a)))])
 
 # Check -- C_0 - (X + C_1) ==> (C_0 + C1) + X
-# RUN: grep -A 2 \"# Query 15$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 10 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 15$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 20 (Add w8 (Read w8 0 a) 10))])
 
 # Check -- C_0 - (C_1 - X) ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 16$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 10 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 16$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 10 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 20 (Sub w8 10 (Read w8 0 a)))])
 
 # Check -- C_0 - (X - C_1) ==> (C_0 + C1) - X
-# RUN: grep -A 2 \"# Query 17$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 30 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 17$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 20 (Sub w8 (Read w8 0 a) 10))])
 
 # Check -- (C_0 + X) - C_1 ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 18$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 18$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 (Add w8 10 (Read w8 0 a)) 20)])
 
 # Check -- (X + C_0) - C_1 ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 19$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 19$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 (Add w8 (Read w8 0 a) 10) 20)])
 
 # Check -- (C_0 - X) - C_1 ==> (C_0 - C1) - X
-# RUN: grep -A 2 \"# Query 20$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 246 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 20$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 246 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 (Sub w8 10 (Read w8 0 a)) 20)])
 
 # Check -- (X - C_0) - C_1 ==> -(C_0 + C1) + X
-# RUN: grep -A 2 \"# Query 21$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 226 (Read w8 0 a))\" %t2
+# RUN: grep -A 2 "# Query 21$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 226 (Read w8 0 a))" %t2
 (query [] false [(Sub w8 (Sub w8 (Read w8 0 a) 10) 20)])
 
 # Check -- (X + Y) - Z ==> X + (Y - Z)
-# RUN: grep -A 3 \"# Query 22$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 1 a) (Read w8 2 a)\" %t2
+# RUN: grep -A 3 "# Query 22$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2
+# RUN: grep                          "(Sub w8 (Read w8 1 a) (Read w8 2 a)" %t2
 (query [] false [(Sub w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- (X - Y) - Z ==> X - (Y + Z)
-# RUN: grep -A 3 \"# Query 23$\" %t > %t2
-# RUN: grep \"(query .. false .(Sub w8 (Read w8 0 a)\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 1 a) (Read w8 2 a)\" %t2
+# RUN: grep -A 3 "# Query 23$" %t > %t2
+# RUN: grep "(query .. false .(Sub w8 (Read w8 0 a)" %t2
+# RUN: grep                          "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2
 (query [] false [(Sub w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- X - (C + Y) ==> -C + (X - Y)
-# RUN: grep -A 3 \"# Query 24$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 24$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246" %t2
+# RUN: grep                          "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))])
 
 # Check -- X - (Y + C) ==> -C + (X - Y)
-# RUN: grep -A 3 \"# Query 25$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 25$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246" %t2
+# RUN: grep                          "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))])
 
 # Check -- X - (C - Y) ==> -C + (X + Y)
-# RUN: grep -A 3 \"# Query 26$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 246\" %t2
-# RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 26$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 246" %t2
+# RUN: grep                          "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))])
 
 # Check -- X - (Y - C) ==> C + (X - Y)
-# RUN: grep -A 3 \"# Query 27$\" %t > %t2
-# RUN: grep \"(query .. false .(Add w8 10\" %t2
-# RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
+# RUN: grep -A 3 "# Query 27$" %t > %t2
+# RUN: grep "(query .. false .(Add w8 10" %t2
+# RUN: grep                          "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))])
 
 # Check -- X * 0 ==> 0
-# RUN: grep -A 2 \"# Query 28$\" %t > %t2
-# RUN: grep \"(query .. false .(w8 0).\" %t2
+# RUN: grep -A 2 "# Query 28$" %t > %t2
+# RUN: grep "(query .. false .(w8 0)." %t2
 (query [] false [(Mul w8 0 (Read w8 0 a))])
 
 # Check -- X * 1 ==> X
-# RUN: grep -A 2 \"# Query 29$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+# RUN: grep -A 2 "# Query 29$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a)." %t2
 (query [] false [(Mul w8 1 (Read w8 0 a))])
 
 # Check -- X & 0 ==> 0
-# RUN: grep -A 2 \"# Query 30$\" %t > %t2
-# RUN: grep \"(query .. false .(w8 0).\" %t2
+# RUN: grep -A 2 "# Query 30$" %t > %t2
+# RUN: grep "(query .. false .(w8 0)." %t2
 (query [] false [(And w8 0 (Read w8 0 a))])
 
 # Check -- X & 0b1...1 ==> X
-# RUN: grep -A 2 \"# Query 31$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+# RUN: grep -A 2 "# Query 31$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a)." %t2
 (query [] false [(And w8 255 (Read w8 0 a))])
 
 # Check -- X | 0 ==> X
-# RUN: grep -A 2 \"# Query 32$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+# RUN: grep -A 2 "# Query 32$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a)." %t2
 (query [] false [(Or w8 0 (Read w8 0 a))])
 
 # Check -- X | 0b1...1 ==> X
-# RUN: grep -A 2 \"# Query 33$\" %t > %t2
-# RUN: grep \"(query .. false .(w8 255).\" %t2
+# RUN: grep -A 2 "# Query 33$" %t > %t2
+# RUN: grep "(query .. false .(w8 255)." %t2
 (query [] false [(Or w8 255 (Read w8 0 a))])
 
 # Check -- X ^ 0b1...1 ==> X
-# RUN: grep -A 2 \"# Query 34$\" %t > %t2
-# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+# RUN: grep -A 2 "# Query 34$" %t > %t2
+# RUN: grep "(query .. false .(Read w8 0 a)." %t2
 (query [] false [(Xor w8 0 (Read w8 0 a))])
 
 # Check -- true == X ==> X
-# RUN: grep -A 2 \"# Query 35$\" %t > %t2
-# RUN: grep \"(query .. false .(Eq 0 (Read w8 0 a)).\" %t2
+# RUN: grep -A 2 "# Query 35$" %t > %t2
+# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2
 (query [] false [(Eq true (Eq 0 (Read w8 0 a)))])
 
 # Check -- !!X ==> X
-# RUN: grep -A 2 \"# Query 36$\" %t > %t2
-# RUN: grep \"(query .. false .(Eq 0 (Read w8 0 a)).\" %t2
+# RUN: grep -A 2 "# Query 36$" %t > %t2
+# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2
 (query [] false [(Not (Not (Eq 0 (Read w8 0 a))))])
 
 # Check -- !Const
-# RUN: grep -A 2 \"# Query 37$\" %t > %t2
-# RUN: grep \"(query .. false .true.\" %t2
+# RUN: grep -A 2 "# Query 37$" %t > %t2
+# RUN: grep "(query .. false .true." %t2
 (query [] false [(Eq (Not w32 0xdeadbeef) 0x21524110)])
diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.pc
index ea2e7a5d..71f0288f 100644
--- a/test/Expr/Parser/MultiByteReads.pc
+++ b/test/Expr/Parser/MultiByteReads.pc
@@ -1,6 +1,6 @@
-# RUN: %kleaver -print-ast -pc-multibyte-reads=true %s >log
-# RUN: grep -q "(ReadLSB w32 4 arr1)" log
-# RUN: grep -q "(ReadMSB w32 2 arr2)" log
+# RUN: %kleaver -print-ast -pc-multibyte-reads=true %s > %t.log
+# RUN: grep -q "(ReadLSB w32 4 arr1)" %t.log
+# RUN: grep -q "(ReadMSB w32 2 arr2)" %t.log
 
 array arr1[8] : w32 -> w8 = symbolic
 array arr2[8] : w32 -> w8 = symbolic
diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.pc
index 1a853b16..6d817b6f 100644
--- a/test/Expr/Parser/Simplify.pc
+++ b/test/Expr/Parser/Simplify.pc
@@ -3,38 +3,38 @@
 array a[64] : w32 -> w8 = symbolic
 
 # Check -- X u> Y ==> Y u< X
-# RUN: grep -A 2 \"# Query 1\" %t > %t2
-# RUN: grep \"(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 1" %t > %t2
+# RUN: grep "(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)" %t2
 (query [] false [(Ugt (Read w8 0 a) (Read w8 1 a))])
 
 # Check -- X u>= Y ==> Y u<= X
-# RUN: grep -A 2 \"# Query 2\" %t > %t2
-# RUN: grep \"(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 2" %t > %t2
+# RUN: grep "(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)" %t2
 (query [] false [(Uge (Read w8 0 a) (Read w8 1 a))])
 
 # Check -- X u> Y ==> Y u< X
-# RUN: grep -A 2 \"# Query 3\" %t > %t2
-# RUN: grep \"(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 3" %t > %t2
+# RUN: grep "(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)" %t2
 (query [] false [(Sgt (Read w8 0 a) (Read w8 1 a))])
 
 # Check -- X u>= Y ==> Y u<= X
-# RUN: grep -A 2 \"# Query 4\" %t > %t2
-# RUN: grep \"(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)\" %t2
+# RUN: grep -A 2 "# Query 4" %t > %t2
+# RUN: grep "(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)" %t2
 (query [] false [(Sge (Read w8 0 a) (Read w8 1 a))])
 
 # Check -- X != Y ==> !(X == Y)
-# RUN: grep -A 2 \"# Query 5\" %t > %t2
-# RUN: grep \"(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)\" %t2
+# RUN: grep -A 2 "# Query 5" %t > %t2
+# RUN: grep "(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)" %t2
 (query [] false [(Ne (Read w8 0 a) (Read w8 1 a))])
 
 # Check -- !(X or Y) ==> !X and !Y
-# RUN: grep -A 3 \"# Query 6$\" %t > %t2
-# RUN: grep \"(query .. false .(And (Not (Eq 0 (Read w8 0 a)))\" %t2
-# RUN: grep                       \"(Not (Eq 1 (Read w8 1 a))))\" %t2
+# RUN: grep -A 3 "# Query 6$" %t > %t2
+# RUN: grep "(query .. false .(And (Not (Eq 0 (Read w8 0 a)))" %t2
+# RUN: grep                       "(Not (Eq 1 (Read w8 1 a))))" %t2
 (query [] false [(Not (Or (Eq 0 (Read w8 0 a))
                           (Eq 1 (Read w8 1 a))))])
 
 # Check -- false == X ==> !X
-# RUN: grep -A 2 \"# Query 7\" %t > %t2
-# RUN: grep \"(query .. false .(Not (Extract 1 (Read w8 0 a))).)\" %t2
+# RUN: grep -A 2 "# Query 7" %t > %t2
+# RUN: grep "(query .. false .(Not (Extract 1 (Read w8 0 a))).)" %t2
 (query [] false [(Eq (Extract w1 1 (Read w8 0 a)) false)])
diff --git a/test/Expr/Parser/dg.exp b/test/Expr/Parser/dg.exp
deleted file mode 100644
index 94fc4df8..00000000
--- a/test/Expr/Parser/dg.exp
+++ /dev/null
@@ -1,3 +0,0 @@
-load_lib llvm.exp
-
-RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]]
diff --git a/test/Expr/dg.exp b/test/Expr/dg.exp
deleted file mode 100644
index 94fc4df8..00000000
--- a/test/Expr/dg.exp
+++ /dev/null
@@ -1,3 +0,0 @@
-load_lib llvm.exp
-
-RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]]
diff --git a/test/Expr/print-smt.smt2.good b/test/Expr/print-smt.smt2.good
index cca282af..7b2002b9 100644
--- a/test/Expr/print-smt.smt2.good
+++ b/test/Expr/print-smt.smt2.good
@@ -859,9 +859,9 @@
 ;SMTLIBv2 Query 72
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr2 (_ bv0 32) ) (_ bv121 8) ) )
 (assert (=  (select const_arr2 (_ bv1 32) ) (_ bv101 8) ) )
 (assert (=  (select const_arr2 (_ bv2 32) ) (_ bv115 8) ) )
@@ -881,8 +881,8 @@
 ;SMTLIBv2 Query 73
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  false (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed ?B0 ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
@@ -898,9 +898,9 @@
 ;SMTLIBv2 Query 74
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr5 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr5 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv2 32) ) (_ bv171 8) ) )
@@ -920,9 +920,9 @@
 ;SMTLIBv2 Query 75
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr1 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr1 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr1 (_ bv2 32) ) (_ bv0 8) ) )
@@ -954,9 +954,9 @@
 ;SMTLIBv2 Query 76
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr4 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr4 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv2 32) ) (_ bv171 8) ) )
@@ -976,9 +976,9 @@
 ;SMTLIBv2 Query 77
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr3 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr3 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr3 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr3 (_ bv2 32) ) (_ bv0 8) ) )
@@ -1010,8 +1010,8 @@
 ;SMTLIBv2 Query 78
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533328 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed_1 (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed_1 ?B0 ) ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-09-19 11:58:29 +0000