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)) + ) + ) + ) ) ) )