From b40bfc49ba0ea68e58f1c75964bf9fcacd76c0e3 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 27 Sep 2023 17:05:23 -0700 Subject: [PATCH] add horn versions of map/str tests --- tests/horn/pos/maps00.smt2 | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/horn/pos/maps00.smt2 b/tests/horn/pos/maps00.smt2 index 973d0d4bb..b09679a50 100644 --- 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)) + ) + ) + ) ) ) )