From 285d60dda0ae4fe16f4827500cb727da5fcbb4d6 Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Fri, 16 Nov 2018 16:27:00 +0100
Subject: [PATCH] ce transformation: Disable projections of records

---
 .../ce/oracles/record_map_CVC4,1.5_SP.oracle  | 64 ++-----------------
 .../ce/oracles/record_map_CVC4,1.5_WP.oracle  | 64 ++-----------------
 .../ce/oracles/record_map_Z3,4.6.0_SP.oracle  | 50 ++-------------
 .../ce/oracles/record_map_Z3,4.6.0_WP.oracle  | 50 ++-------------
 .../intro_projections_counterexmp.ml          |  2 +-
 5 files changed, 21 insertions(+), 209 deletions(-)

diff --git a/bench/ce/oracles/record_map_CVC4,1.5_SP.oracle b/bench/ce/oracles/record_map_CVC4,1.5_SP.oracle
index 991ba7d9b7..729023d5cd 100644
--- a/bench/ce/oracles/record_map_CVC4,1.5_SP.oracle
+++ b/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 } }] } }
 
diff --git a/bench/ce/oracles/record_map_CVC4,1.5_WP.oracle b/bench/ce/oracles/record_map_CVC4,1.5_WP.oracle
index 36a623222e..2753a518d1 100644
--- a/bench/ce/oracles/record_map_CVC4,1.5_WP.oracle
+++ b/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 } }] } }
 
diff --git a/bench/ce/oracles/record_map_Z3,4.6.0_SP.oracle b/bench/ce/oracles/record_map_Z3,4.6.0_SP.oracle
index eba9de10ee..9299b71919 100644
--- a/bench/ce/oracles/record_map_Z3,4.6.0_SP.oracle
+++ b/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 }
 
diff --git a/bench/ce/oracles/record_map_Z3,4.6.0_WP.oracle b/bench/ce/oracles/record_map_Z3,4.6.0_WP.oracle
index 1fa51fbd9e..a41bc493ca 100644
--- a/bench/ce/oracles/record_map_Z3,4.6.0_WP.oracle
+++ b/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 }
 
diff --git a/src/transform/intro_projections_counterexmp.ml b/src/transform/intro_projections_counterexmp.ml
index 98beb91874..02080701ee 100644
--- a/src/transform/intro_projections_counterexmp.ml
+++ b/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
 
-- 
GitLab