Skip to content
Snippets Groups Projects
Commit 4153a660 authored by François Bobot's avatar François Bobot
Browse files

Add regression test for #39

parent 63ff04db
No related branches found
No related tags found
1 merge request!20Add regression test for #39
Pipeline #37052 passed
(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)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment