Commit 9c269141 authored by Sylvain Dailler's avatar Sylvain Dailler

Update ce-bench and remove display of stdlib location.

parent 215fea13
......@@ -39,7 +39,12 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' >> "$f.out"
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
printf "SP $2 ($1)... "
echo "Strongest Postcondition" >> "$f.out"
$dir/../bin/why3prove.opt --debug print_model_attrs --debug vc_sp -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
......@@ -48,7 +53,12 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' >> "$f.out"
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
else
......
......@@ -44,6 +44,7 @@ l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
......@@ -90,3 +91,4 @@ l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
......@@ -34,11 +34,11 @@ Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "165" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "163" },
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "161" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "159" },
"list" : [{"type" : "Integer" , "val" : "156" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "154" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......@@ -56,6 +56,7 @@ l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
......@@ -92,11 +93,11 @@ Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
"list" : [{"type" : "Integer" , "val" : "154" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
"list" : [{"type" : "Integer" , "val" : "150" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "148" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......@@ -114,3 +115,4 @@ l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
......@@ -65,7 +65,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......@@ -93,7 +95,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......@@ -121,7 +125,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......@@ -285,7 +291,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......@@ -306,7 +314,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......@@ -327,7 +337,9 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a],
[@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" ,
......
......@@ -27,7 +27,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
......@@ -53,7 +55,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
......@@ -79,7 +83,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
......@@ -123,7 +129,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
......@@ -145,7 +153,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
......@@ -167,7 +177,9 @@ Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
......
......@@ -62,19 +62,33 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
bench/ce/records.mlw M VC record_match_eval_test44: Timeout or Unknown
Counter-example model:File records.mlw:
Line 38:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 42:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC record_match_eval_test44: Valid
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
Counter-example model:File records.mlw:
Line 45:
re, [[@introduced], [@model_trace:re]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 40:
Line 47:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 41:
Line 48:
re, [[@introduced], [@model_trace:re]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
......@@ -84,7 +98,7 @@ x, [[@introduced],
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 43:
Line 50:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
......@@ -92,13 +106,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Timeout or Unknown
Counter-example model:File records.mlw:
Line 57:
Line 64:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 58:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -108,13 +122,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Timeout or Unknown
Counter-example model:File records.mlw:
Line 65:
Line 72:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 66:
Line 73:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -123,19 +137,19 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test3: Timeout or Unknown
Counter-example model:File records.mlw:
Line 70:
Line 77:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 71:
Line 78:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 73:
Line 80:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -144,19 +158,19 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test4: Timeout or Unknown
Counter-example model:File records.mlw:
Line 75:
Line 82:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 76:
Line 83:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
Line 85:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -217,19 +231,33 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
bench/ce/records.mlw M VC record_match_eval_test44: Timeout or Unknown
Counter-example model:File records.mlw:
Line 38:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 42:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC record_match_eval_test44: Valid
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
Counter-example model:File records.mlw:
Line 45:
re, [[@introduced], [@model_trace:re]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 40:
Line 47:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 41:
Line 48:
re, [[@introduced], [@model_trace:re]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "6" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
......@@ -242,13 +270,13 @@ x, [[@introduced],
bench/ce/records.mlw Mutable VC record_match_eval_test1: Timeout or Unknown
Counter-example model:File records.mlw:
Line 57:
Line 64:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 58:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -258,13 +286,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Timeout or Unknown
Counter-example model:File records.mlw:
Line 65:
Line 72:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 66:
Line 73:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -273,13 +301,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test3: Timeout or Unknown
Counter-example model:File records.mlw:
Line 70:
Line 77:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 71:
Line 78:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -288,13 +316,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test4: Timeout or Unknown
Counter-example model:File records.mlw:
Line 75:
Line 82:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 76:
Line 83:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......
......@@ -49,36 +49,50 @@ x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" , "type" : "Proj" ,
"value" : {"type" : "Boolean" ,
"val" : false } }
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
bench/ce/records.mlw M VC record_match_eval_test44: Timeout or Unknown
Counter-example model:File records.mlw:
Line 38:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "2" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 42:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "2" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC record_match_eval_test44: Valid
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
Counter-example model:File records.mlw:
Line 45:
re, [[@introduced], [@model_trace:re]] = {"proj_name" : "g" ,
"type" : "Proj" , "value" : {"type" : "Boolean" ,
"val" : false } }
Line 40:
Line 47:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" , "type" : "Proj" ,
"value" : {"type" : "Boolean" , "val" : false } }
Line 41:
Line 48:
re, [[@introduced], [@model_trace:re]] = {"proj_name" : "g" ,
"type" : "Proj" , "value" : {"type" : "Boolean" ,
"val" : false } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" ,
"type" : "Proj" , "value" : {"type" : "Boolean" ,
"val" : false } }
Line 43:
Line 50:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" , "type" : "Proj" ,
"value" : {"type" : "Boolean" ,
"val" : false } }
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (sat)
Counter-example model:File records.mlw:
Line 57:
Line 64:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 58:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -88,13 +102,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (sat)
Counter-example model:File records.mlw:
Line 65:
Line 72:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 66:
Line 73:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -103,19 +117,19 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (sat)
Counter-example model:File records.mlw:
Line 70:
Line 77:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 71:
Line 78:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 73:
Line 80:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -124,19 +138,19 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (sat)
Counter-example model:File records.mlw:
Line 75:
Line 82:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 76:
Line 83:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
Line 85:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -188,16 +202,30 @@ x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" , "type" : "Proj" ,
"value" : {"type" : "Boolean" ,
"val" : false } }
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
bench/ce/records.mlw M VC record_match_eval_test44: Timeout or Unknown
Counter-example model:File records.mlw:
Line 38:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "2" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 42:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"type" : "Integer" ,
"val" : "2" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw M VC record_match_eval_test44: Valid
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout or Unknown
Counter-example model:File records.mlw:
Line 45:
re, [[@introduced], [@model_trace:re]] = {"proj_name" : "g" ,
"type" : "Proj" , "value" : {"type" : "Boolean" ,
"val" : false } }
Line 40:
Line 47:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" , "type" : "Proj" ,
"value" : {"type" : "Boolean" , "val" : false } }
Line 41:
Line 48:
re, [[@introduced], [@model_trace:re]] = {"proj_name" : "g" ,
"type" : "Proj" , "value" : {"type" : "Boolean" ,
"val" : false } }
......@@ -207,13 +235,13 @@ x, [[@introduced], [@model_trace:x]] = {"proj_name" : "g" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (sat)
Counter-example model:File records.mlw:
Line 57:
Line 64:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 58:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -223,13 +251,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (sat)
Counter-example model:File records.mlw:
Line 65:
Line 72:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 66:
Line 73:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
......@@ -238,13 +266,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (sat)
Counter-example model:File records.mlw:
Line 70:
Line 77:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 71:
Line 78:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......@@ -253,13 +281,13 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (sat)
Counter-example model:File records.mlw:
Line 75:
Line 82:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 76:
Line 83:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
......
......@@ -4,12 +4,14 @@ Counter-example model:File ref.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 9:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
......@@ -20,52 +22,71 @@ Counter-example model:File ref.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "-42" }
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 13:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "42" }
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 15:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "0" }
"val" : "42" }
bench/ce/ref.mlw M VC incr: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 21:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "-1" }
Line 23:
x23, [[@introduced], [@model_trace:x23]] = {"type" : "Integer" ,
"val" : "-2" }
x23, [[@introduced], [@model_trace:x23],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 24:
x23, [[@introduced], [@model_trace:x23]] = {"type" : "Integer" ,
"val" : "2" }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "0" }
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "0" }
Line 28:
x23, [[@introduced], [@model_trace:x23]] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "1" }
Line 29:
x23, [[@introduced], [@model_trace:x23]] = {"type" : "Integer" ,
"val" : "0" }
"val" : "2" }
bench/ce/ref.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 21:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "-2" }
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced], [@model_trace:x], [@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 38:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"type" : "Integer" ,
"val" : "0" }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"type" : "Integer" ,
"val" : "0" }
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
......@@ -73,18 +94,27 @@ bench/ce/ref.mlw M VC test_loop: Valid
bench/ce/ref.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 21:
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Integer" ,
"val" : "-2" }
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced], [@model_trace:x], [@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"type" : "Integer" ,
"val" : "0" }
Line 37:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
Line 38:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"type" : "Integer" ,
"val" : "0" }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"type" : "Integer" ,
"val" : "0" }
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
Line 40:
......@@ -94,16 +124,23 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
bench/ce/ref.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref.mlw: