Commit 4a1fdcae authored by Clément Fumex's avatar Clément Fumex

- stop reporting z3.2-19 warnings as errors

- change the syntax converter of z3 for bitvectors
  (z3 get confused if there is a variable "bv1" and then a declaration
  (_ bv1 32))
parent 20695e08
......@@ -6,7 +6,7 @@ printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
fail "^(error \"\\(.*\\)\")" "Error: \1"
fail "^(error \"\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\)\\(.*\\)\")" "Error: \1"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
valid "^unsat"
......
......@@ -56,7 +56,7 @@ theory bitvec.BitVector64
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 64)"
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -121,7 +121,7 @@ theory bitvec.BitVector32
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 32)"
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -186,7 +186,7 @@ theory bitvec.BitVector16
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 16)"
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......@@ -251,7 +251,7 @@ theory bitvec.BitVector8
syntax function lsr "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 8)"
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_int "(bv2int %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
......
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