Commit ffa0aa01 authored by Andrei Paskevich's avatar Andrei Paskevich

keep the Z3 driver closer to the previous version

parent acc08f43
...@@ -109,7 +109,7 @@ theory real.Real ...@@ -109,7 +109,7 @@ theory real.Real
end end
theory bool.Bool theory bool.Bool
syntax type bool "bool" syntax type bool "Bool"
syntax function True "true" syntax function True "true"
syntax function False "false" syntax function False "false"
syntax function andb "(and %1 %2)" syntax function andb "(and %1 %2)"
...@@ -150,7 +150,7 @@ theory map.Map ...@@ -150,7 +150,7 @@ theory map.Map
syntax type map "(Array %1 %2)" syntax type map "(Array %1 %2)"
meta "encoding : lskept" function get meta "encoding : lskept" function get
meta "encoding : lskept" function set meta "encoding : lskept" function set
(* meta "encoding : lskept" function const *) meta "encoding : lskept" function const
syntax function get "(select %1 %2)" syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)" syntax function set "(store %1 %2 %3)"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment