diff --git a/tests/sat/arr.smt2 b/tests/sat/arr.smt2 new file mode 100644 index 0000000000000000000000000000000000000000..ad58211f5b92c814aaff9afdd49dea7206205e48 --- /dev/null +++ b/tests/sat/arr.smt2 @@ -0,0 +1,27 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) + + +(declare-sort u 0) + +(declare-fun to_rep (u) Int) + +(declare-sort t 0) + +(declare-fun mk ((Array Int u) Bool) t) + +(declare-fun get_a (t) (Array Int u)) + +(declare-fun get_b (t) Bool) +(declare-const rliteral u) + +(declare-const r t) + + +(assert + (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 3)) 5)) + +(assert + (not + (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 1)) 5))) +(check-sat)