Commit 48793c5b authored by DAILLER Sylvain's avatar DAILLER Sylvain

Range projection meta

parent c7cdf962
Strongest Postcondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 13:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 15:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 17:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 19:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 21:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 31:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 33:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 37:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 39:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 41:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 43:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 45:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 49:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 13:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 15:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 17:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 19:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 21:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 31:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 33:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 37:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "5\/4" } }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 39:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Fraction" ,
"val" : "17\/4" } }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 41:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 43:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 45:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [[@model_trace:zeroF]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
File floats.mlw:
Line 49:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Strongest Postcondition
bench/ce/range_type.mlw Range_int VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
bench/ce/range_type.mlw Range_float VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 20:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Weakest Precondition
bench/ce/range_type.mlw Range_int VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
bench/ce/range_type.mlw Range_float VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 20:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
Strongest Postcondition
bench/ce/range_type.mlw Range_int VC f: Unknown (sat)
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
bench/ce/range_type.mlw Range_float VC f: Unknown (sat)
Counter-example model:File range_type.mlw:
Line 20:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Decimal" ,
"val" : "10.0" } }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Decimal" ,
"val" : "10.0" } }
Weakest Precondition
bench/ce/range_type.mlw Range_int VC f: Unknown (sat)
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
bench/ce/range_type.mlw Range_float VC f: Unknown (sat)
Counter-example model:File range_type.mlw:
Line 20:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Decimal" ,
"val" : "10.0" } }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
"type" : "Proj" , "value" : {"type" : "Decimal" ,
"val" : "10.0" } }
module Range_int
use int.Int
type int32 = < range -0x8000_0000 0x7fff_ffff >
let f (x: int32)
=
assert {int32'int x < 5}
end
module Range_float
use real.Real
type t = < float 8 24 >
let f (x: t)
=
assert {t'real x < 10.}
end
\ No newline at end of file
......@@ -173,7 +173,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.20" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.22"/></proof>
<proof prover="11"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
......
......@@ -650,7 +650,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" expl="rewrite premises" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="2.72"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.99"/></proof>
</goal>
</transf>
</goal>
......
......@@ -929,7 +929,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.48" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>