Commit 23300041 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Change parsing for z3 fractions

parent d25dbe07
ce/real.mlw ModelReal test1 : Unknown (other)
Counter-example model:File real.mlw:
Line 5:
x = {"type" : "Fraction" ,
"val" : "1\/2" }
ce/real.mlw ModelReal test2 : Unknown (other)
Counter-example model:File real.mlw:
Line 7:
......
......@@ -211,6 +211,16 @@ decimal:
fraction:
| LPAREN ps DIV ps integer ps integer ps RPAREN
{ ($5, $7) }
(* Integer from z3 can be written 1.0 *)
| LPAREN ps DIV ps decimal ps decimal ps RPAREN
{ let (num, numdot) = $5 in
let (dec, decdot) = $7 in
if numdot = "0" && decdot = "0" then
(num, dec)
else
(* Should not happen. If it does, change the parsing *)
assert (false)
}
(* Example:
(_ bv2048 16) *)
......
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