Commit b28fffa4 authored by MARCHE Claude's avatar MARCHE Claude

bv to smt2: remove extensionality axiom since 'eq' is '='

parent 3b375dd5
......@@ -200,6 +200,7 @@ theory bv.BV32
(* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
(* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
syntax predicate eq "(= %1 %2)"
remove prop Equationality
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
......
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