Commit bc1fd35e authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

from_int is a coercion in CVC3

parent 709f590a
...@@ -110,6 +110,19 @@ theory real.Real ...@@ -110,6 +110,19 @@ theory real.Real
end end
theory real.FromInt
syntax function from_int "%1"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
theory bool.Bool theory bool.Bool
syntax type bool "BITVECTOR(1)" syntax type bool "BITVECTOR(1)"
syntax function True "0bin1" syntax function True "0bin1"
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