Skip to content

GitLab

why3
why3
Commit 58f09fef authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

BV theory: reverted removal of normally useless axiom

parent ce356884
Hide whitespace changes
Inline Side-by-side
Showing with 4 additions and 4 deletions
theories/bv.why
View file @ 58f09fef
......@@ -404,7 +404,7 @@ theory BV64
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -420,7 +420,7 @@ theory BV32
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -436,7 +436,7 @@ theory BV16
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -452,7 +452,7 @@ theory BV8
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
(* meta "remove_prop" prop size_pos *)
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......
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