1 files changed, 28 insertions, 0 deletions
diff --git a/test/Expr/Evaluate.kquery b/test/Expr/Evaluate.kquery
new file mode 100644
index 00000000..43134475
--- /dev/null
+++ b/test/Expr/Evaluate.kquery
@@ -0,0 +1,28 @@
+# RUN: %kleaver -evaluate %s > %t.log
+
+array arr0[4] : w32 -> w8 = symbolic
+array arr1[8] : w32 -> w8 = symbolic
+
+# RUN: grep "Query 0:	INVALID" %t.log
+# Query 0
+(query [] (Not (Ult (ReadLSB w32 0 arr0)
+                    16)))
+
+# RUN: grep "Query 1:	VALID" %t.log
+# Query 1
+(query [(Eq N0:(ReadLSB w32 0 arr1) 10)
+        (Eq N1:(ReadLSB w32 4 arr1) 20)]
+       (Eq (Add w32 N0 N1)
+           30))
+
+# RUN: grep "Query 2:	VALID" %t.log
+# Query 2
+array hello[4] : w32 -> w8 = [ 1 2 3 5 ]
+(query [] (Eq (Add w8 (Read w8 0 hello)
+                      (Read w8 3 hello))
+              6))
+
+# RUN: grep "Query 3:	VALID" %t.log
+# Query 2
+(query [] (Eq (Not w8 (Read w8 0 arr1))
+              (Xor w8 (Read w8 0 arr1) 0xff)))