Skip to content

GitLab

why3
why3
Commit 68ca69f9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

fix stupid bug introduced in previous commit...

parent b28fffa4
Show whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
drivers/smt-libv2.drv
View file @ 68ca69f9
......@@ -200,7 +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
remove prop Extensionality
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