Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }