ce transformation: Disable projections of records

bench/ce/oracles/record_map_CVC4,1.5_SP.oracle

@@ -32,14 +32,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 47:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
@@ -48,14 +40,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 
 bench/ce/record_map.mlw M VC record_map_proj_test3: Timeout or Unknown
 Counter-example model:File record_map.mlw:
@@ -63,63 +47,27 @@ Line 51:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 53:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
-"val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
+"val" : true } }] } }
 Line 54:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
-"val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
+"val" : true } }] } }
 

bench/ce/oracles/record_map_CVC4,1.5_WP.oracle

@@ -32,14 +32,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 47:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
@@ -48,14 +40,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 
 bench/ce/record_map.mlw M VC record_map_proj_test3: Timeout or Unknown
 Counter-example model:File record_map.mlw:
@@ -63,63 +47,27 @@ Line 51:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 53:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
-"val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
+"val" : true } }] } }
 Line 54:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
-"val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"indice" : "true" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
+"val" : true } }] } }
 

bench/ce/oracles/record_map_Z3,4.6.0_SP.oracle

@@ -25,13 +25,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 47:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
@@ -39,13 +32,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 
 bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (sat)
 Counter-example model:File record_map.mlw:
@@ -53,55 +39,27 @@ Line 51:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 53:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 54:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 

bench/ce/oracles/record_map_Z3,4.6.0_WP.oracle

@@ -25,13 +25,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 47:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
@@ -39,13 +32,6 @@ rec_map, [[@model_projected], [@introduced],
 "val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 
 bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (sat)
 Counter-example model:File record_map.mlw:
@@ -53,55 +39,27 @@ Line 51:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 53:
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 Line 54:
 re_rec_map, [[@model_projected], [@introduced],
 [@model_trace:re_rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-re_rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "0" } }] }
-re_rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:re_rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 rec_map, [[@model_projected], [@introduced],
 [@model_trace:rec_map]] = {"type" : "Record" ,
 "val" : {"Field" : [{"field" : "f_map" , "value" : {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" , "val" : "1" } }] } },
+"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
 {"field" : "g_bool" , "value" : {"type" : "Boolean" ,
 "val" : false } }] } }
-rec_map.f_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.f_map]] = {"type" : "Array" ,
-"val" : [{"others" : {"type" : "Integer" ,
-"val" : "1" } }] }
-rec_map.g_map, [[@model_projected], [@introduced],
-[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
-"val" : false }
 

src/transform/intro_projections_counterexmp.ml

@@ -16,7 +16,7 @@ open Theory
 open Ty
 
 let is_proj_for_array_attr proj_name =
-  match Str.search_forward (Str.regexp "'First\\|'Last\\|\\.") proj_name 0 with
+  match Str.search_forward (Str.regexp "'First\\|'Last") proj_name 0 with
   | _ -> true
   | exception Not_found -> false