CE: add default model attribute also on logic constants

bench/ce/floats_CVC4,1.5.oracle

 bench/ce/floats.mlw T32 g1: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g2: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g3: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g4: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g5: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g6: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g7: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g8: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g9: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T32 g10: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g1: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g2: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g3: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g4: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g5: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g6: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g7: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g8: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g9: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+
 bench/ce/floats.mlw T64 g10: Timeout
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "-1" }
+

bench/ce/floats_Z3,4.6.0.oracle

 bench/ce/floats.mlw T32 g1: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 5:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x1.000002p-126" ,
 "value" : -1.17549e-38 } }
 
 bench/ce/floats.mlw T32 g2: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 7:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x0.008000p-127" ,
 "value" : -1.14794e-41 } }
 
 bench/ce/floats.mlw T32 g3: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 9:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Minus_zero" } }
 
 bench/ce/floats.mlw T32 g4: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 11:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.400000p0" ,
 "value" : 1.25 } }
 
 bench/ce/floats.mlw T32 g5: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 13:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.000002p65" ,
 "value" : 3.68935e+19 } }
 
 bench/ce/floats.mlw T32 g6: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 15:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Not_a_number" } }
 
 bench/ce/floats.mlw T32 g7: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 17:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x1.800000p32" ,
 "value" : -6.44245e+09 } }
 
 bench/ce/floats.mlw T32 g8: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 19:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Plus_infinity" } }
 
 bench/ce/floats.mlw T32 g9: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 21:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x0.000002p-127" ,
 "value" : 7.00649e-46 } }
 
 bench/ce/floats.mlw T32 g10: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 23:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.99999ap-4" ,
 "value" : 0.1 } }
 
 bench/ce/floats.mlw T64 g1: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 31:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x1.0000000000001p-1022" ,
 "value" : -2.22507e-308 } }
 
 bench/ce/floats.mlw T64 g2: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 33:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x0.0000040000000p-1023" ,
 "value" : -2.65249e-315 } }
 
 bench/ce/floats.mlw T64 g3: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 35:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Minus_zero" } }
 
 bench/ce/floats.mlw T64 g4: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 37:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.4000000000000p0" ,
 "value" : 1.25 } }
 
 bench/ce/floats.mlw T64 g5: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 39:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.0000000000001p513" ,
 "value" : 2.68156e+154 } }
 
 bench/ce/floats.mlw T64 g6: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 41:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Not_a_number" } }
 
 bench/ce/floats.mlw T64 g7: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 43:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "-0x1.0000000000000p54" ,
 "value" : -1.80144e+16 } }
 
 bench/ce/floats.mlw T64 g8: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 45:
 x = {"type" : "Float" ,
 "val" : {"cons" : "Plus_infinity" } }
 
 bench/ce/floats.mlw T64 g9: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 47:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x0.0000000000001p-1023" ,
 "value" : 0 } }
 
 bench/ce/floats.mlw T64 g10: Timeout
-Counter-example model:File floats.mlw:
+Counter-example model:File ieee_float.mlw:
+Line 218:
+max_int = {"type" : "Integer" ,
+"val" : "5" }
+File floats.mlw:
 Line 49:
 x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
 "str_hexa" : "0x1.999999999999ap-4" ,

bench/ce/int.mlw

@@ -2,16 +2,15 @@ theory T
 
   use import int.Int
 
-  goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50
+  goal g_lab : forall x [@model] :int. x >= 42 -> x + 3 <= 50
 
-  goal g_lab0 : forall x:int. (x >= 42) ->
-    (x + 3 <= 50)
+  goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50
 
   constant g : int
 
   goal g2_lab : forall x:int. (g >= x)
 
-  goal newgoal : forall x1 [@model_trace:X] x2 x3 x4 x5 x6 x7 x8.
+  goal newgoal : forall x1 [@model] [@model_trace:X] x2 x3 x4 x5 x6 x7 x8.
   (x1 + 1 = 2) ->
   (x2 + 1 = 2) ->
   (x3 + 1 = 2) ->

bench/ce/int_CVC4,1.5.oracle

-bench/ce/int.mlw T g_no_lab: Unknown (other)
+bench/ce/int.mlw T g_lab: Unknown (other)
 Counter-example model:File int.mlw:
 Line 5:
 x = {"type" : "Integer" ,
 "val" : "48" }
 
-bench/ce/int.mlw T g_lab0: Unknown (other)
+bench/ce/int.mlw T g_no_lab: Unknown (other)
 Counter-example model:File int.mlw:
 Line 7:
 x = {"type" : "Integer" ,
@@ -12,14 +12,20 @@ x = {"type" : "Integer" ,
 
 bench/ce/int.mlw T g2_lab: Unknown (other)
 Counter-example model:File int.mlw:
-Line 12:
+Line 9:
+g = {"type" : "Integer" , "val" : "-1" }
+Line 11:
 x = {"type" : "Integer" ,
 "val" : "0" }
 
 bench/ce/int.mlw T newgoal: Unknown (other)
 Counter-example model:File int.mlw:
-Line 14:
-x2 = {"type" : "Integer" , "val" : "1" }
+Line 9:
+g = {"type" : "Integer" , "val" : "0" }
+Line 13:
+X = {"type" : "Integer" , "val" : "1" }
+x2 = {"type" : "Integer" ,
+"val" : "1" }
 x3 = {"type" : "Integer" ,
 "val" : "1" }
 x4 = {"type" : "Integer" ,

bench/ce/int_Z3,4.6.0.oracle

-bench/ce/int.mlw T g_no_lab: Unknown (other)
+bench/ce/int.mlw T g_lab: Unknown (other)
 Counter-example model:File int.mlw:
 Line 5:
 x = {"type" : "Integer" ,
 "val" : "48" }
 
-bench/ce/int.mlw T g_lab0: Unknown (other)
+bench/ce/int.mlw T g_no_lab: Unknown (other)
 Counter-example model:File int.mlw:
 Line 7:
 x = {"type" : "Integer" ,
@@ -12,14 +12,18 @@ x = {"type" : "Integer" ,
 
 bench/ce/int.mlw T g2_lab: Unknown (other)
 Counter-example model:File int.mlw:
-Line 12:
+Line 9:
+g = {"type" : "Integer" , "val" : "0" }
+Line 11:
 x = {"type" : "Integer" ,
 "val" : "1" }
 
 bench/ce/int.mlw T newgoal: Unknown (other)
 Counter-example model:File int.mlw:
-Line 14:
-x2 = {"type" : "Integer" , "val" : "1" }
+Line 13:
+X = {"type" : "Integer" , "val" : "1" }
+x2 = {"type" : "Integer" ,
+"val" : "1" }
 x3 = {"type" : "Integer" ,
 "val" : "1" }
 x4 = {"type" : "Integer" ,

bench/ce/result.mlw

+
+module M
+
+  use import int.Int
+  use import ref.Ref
+
+  val a : ref int
+
+  let p1 (b : ref int) : int
+    requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 }
+    ensures  { 17 <= !a + result <= 42 }
+  = a := !a + !b;
+    !a + 1
+
+
+let f (a [@model] [@model_trace:A]: ref int)
+  requires { !a = 42 }
+  ensures { !a = 2 + old !a + result } =
+  a := 0;
+  a := 1;
+  !a+1
+
+end
\ No newline at end of file

bench/ce/result_CVC4,1.5.oracle

+bench/ce/result.mlw M VC p1: Unknown (other)
+Counter-example model:File result.mlw:
+Line 7:
+a = {"type" : "Integer" , "val" : "3" }
+Line 9:
+b = {"type" : "Integer" , "val" : "3" }
+Line 11:
+old a = {"type" : "Integer" ,
+"val" : "3" }
+
+bench/ce/result.mlw M VC f: Unknown (other)
+Counter-example model:File result.mlw:
+Line 16:
+A = {"type" : "Integer" , "val" : "1" }
+Line 18:
+old A = {"type" : "Integer" ,
+"val" : "1" }
+

bench/ce/result_Z3,4.6.0.oracle

+bench/ce/result.mlw M VC p1: Timeout
+Counter-example model:File result.mlw:
+Line 7:
+a = {"type" : "Integer" , "val" : "3" }
+Line 9:
+b = {"type" : "Integer" , "val" : "3" }
+Line 11:
+old a = {"type" : "Integer" ,
+"val" : "3" }
+
+bench/ce/result.mlw M VC f: Timeout
+Counter-example model:File result.mlw:
+Line 16:
+A = {"type" : "Integer" , "val" : "1" }
+Line 18:
+old A = {"type" : "Integer" ,
+"val" : "1" }
+

src/parser/parser.mly

@@ -371,7 +371,8 @@ type_case:
 
 constant_decl:
 | labels(lident_rich) cast preceded(EQUAL,term)?
-  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
+  { { ld_ident = add_model_trace_label $1;
+      ld_params = []; ld_type = Some $2;
       ld_def = $3; ld_loc = floc $startpos $endpos } }
 
 function_decl: