ce-bench: Forgotten oracles, fixing diffs

bench/ce/algebraic_type_Z3,4.6.0.oracle

@@ -36,9 +36,9 @@ l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
 {"type" : "Apply" , "val" : {"apply" : "Cons" ,
 "list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
 "val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
+"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
+"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
 {"type" : "Apply" , "val" : {"apply" : "Cons" ,
-"list" : [{"type" : "Integer" , "val" : "156" }, {"type" : "Apply" ,
-"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "154" },
 {"type" : "Apply" , "val" : {"apply" : "Nil" ,
 "list" : [] } }] } }] } }] } }] } }] } }
 
@@ -93,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" : "154" }, {"type" : "Apply" ,
-"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
+"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
+"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
 {"type" : "Apply" , "val" : {"apply" : "Cons" ,
-"list" : [{"type" : "Integer" , "val" : "150" }, {"type" : "Apply" ,
-"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "148" },
+"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
+"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
 {"type" : "Apply" , "val" : {"apply" : "Nil" ,
 "list" : [] } }] } }] } }] } }] } }] } }
 

bench/ce/array_mono_CVC4,1.5.oracle

+Weakest Precondition
+bench/ce/array_mono.mlw Array VC array: Valid
+bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 35:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+Line 36:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+
+bench/ce/array_mono.mlw A VC f2: Valid
+bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 38:
+a, [[@introduced], [@model_trace:a],
+[@at:'Old:loc:location],
+[@at:'Old:loc:location] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 40:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 41:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+
+Strongest Postcondition
+bench/ce/array_mono.mlw Array VC array: Valid
+bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 35:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+Line 36:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+
+bench/ce/array_mono.mlw A VC f2: Valid
+bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 38:
+a, [[@introduced], [@model_trace:a],
+[@at:'Old:loc:location],
+[@at:'Old:loc:location] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 40:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+

bench/ce/array_mono_Z3,4.6.0.oracle

+Weakest Precondition
+bench/ce/array_mono.mlw Array VC array: Valid
+bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 35:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+Line 36:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+
+bench/ce/array_mono.mlw A VC f2: Valid
+bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 38:
+a, [[@introduced], [@model_trace:a],
+[@at:'Old:loc:location],
+[@at:'Old:loc:location] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 40:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 41:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+
+Strongest Postcondition
+bench/ce/array_mono.mlw Array VC array: Valid
+bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 35:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+Line 36:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+{"field" : "length" , "value" : {"type" : "Integer" ,
+"val" : "0" } }] } }
+
+bench/ce/array_mono.mlw A VC f2: Valid
+bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
+Counter-example model:File array_mono.mlw:
+Line 38:
+a, [[@introduced], [@model_trace:a],
+[@at:'Old:loc:location],
+[@at:'Old:loc:location] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+Line 40:
+a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
+"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }] } }
+

bench/ce/record_one_field_CVC4,1.5.oracle

+Weakest Precondition
+bench/ce/record_one_field.mlw Ref VC ref: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC prefix !: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw M VC test_post: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 24:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 25:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 27:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+
+bench/ce/record_one_field.mlw M VC test_post2: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 29:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "42" } }
+Line 31:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "42" } }
+y at 'Old, [[@introduced],
+[@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "42" } }
+Line 33:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "42" } }
+
+bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 41:
+x23, [[@introduced], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 42:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 45:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 46:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 47:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 53:
+x, [[@introduced], [@model_trace:x],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 56:
+x at L, [[@introduced], [@model_trace:x], [@at:L],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x at M, [[@introduced], [@model_trace:x], [@at:M],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x, [[@introduced],
+[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Valid
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+Line 53:
+x, [[@introduced], [@model_trace:x],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "3" } }
+Line 55:
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+Line 56:
+x at L, [[@introduced], [@model_trace:x], [@at:L],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+x at M, [[@introduced], [@model_trace:x], [@at:M],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+x, [[@introduced],
+[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "3" } }
+Line 58:
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+Line 50:
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+Line 53:
+x, [[@introduced], [@model_trace:x],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "-2" } }
+Line 55:
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+
+Strongest Postcondition
+bench/ce/record_one_field.mlw Ref VC ref: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC prefix !: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw M VC test_post: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 24:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 25:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+
+bench/ce/record_one_field.mlw M VC test_post2: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 29:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "42" } }
+Line 31:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "42" } }
+y at 'Old, [[@introduced],
+[@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "42" } }
+
+bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 41:
+x23, [[@introduced], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 42:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+Line 56:
+x at L, [[@introduced], [@model_trace:x], [@at:L],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x at M, [[@introduced], [@model_trace:x], [@at:M],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "2" } }
+x, [[@introduced],
+[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "2" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Valid
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+Line 56:
+x at L, [[@introduced], [@model_trace:x], [@at:L],
+[@at:L:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+x at M, [[@introduced], [@model_trace:x], [@at:M],
+[@at:M:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "3" } }
+x, [[@introduced],
+[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "3" } }
+
+bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+Line 49:
+x, [[@introduced], [@model_trace:x],
+[@at:'Old:loc:location],
+[@at:L:loc:location],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+Line 50:
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "-2" } }
+

bench/ce/record_one_field_Z3,4.6.0.oracle

+Weakest Precondition
+bench/ce/record_one_field.mlw Ref VC ref: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC ref1: Valid
+bench/ce/record_one_field.mlw Ref VC prefix !: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw Ref VC infix :=: Valid
+bench/ce/record_one_field.mlw M VC test_post: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 24:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 25:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "1" }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 27:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+
+bench/ce/record_one_field.mlw M VC test_post2: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 29:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 31:
+x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
+"val" : "43" }
+y, [[@introduced],
+[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "0" } }
+y at 'Old, [[@introduced],
+[@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 33:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+
+bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
+Counter-example model:File record_one_field.mlw:
+Line 39:
+y, [[@introduced], [@model_trace:y],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 41:
+x23, [[@introduced], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 42:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
+[@at:'Old:loc:location] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 45:
+y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 46:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,
+"val" : "0" } }
+Line 47:
+x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
+"type" : "Proj" , "value" : {"type" : "Integer" ,