add horn versions of map/str tests

ucsd-progsys · Sep 28, 2023 · b40bfc4 · b40bfc4
1 parent 19c1952
commit b40bfc4
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/tests/horn/pos/maps00.smt2 b/tests/horn/pos/maps00.smt2
@@ -7,6 +7,19 @@
       (forall ((v Int) (v == (Map_select m1 100)))
         ((v == 0))
       )
+      (forall ((m2 (Map_t Int Int)) (m2 == (Map_store (Map_store m1 10 1) 20 2)))
+        (and
+          (forall ((v Int) (v == (Map_select m2 10)))
+            ((v == 1))
+          )
+          (forall ((v Int) (v == (Map_select m2 20)))
+            ((v == 2))
+          )
+          (forall ((v Int) (v == (Map_select m2 30)))
+            ((v == 0))
+          )
+        )
+      )
     )
   )
 )