Remove model labels in bench/ce

bench/ce/if_decision_branch.mlw

@@ -5,7 +5,7 @@ module Main
 
   type path_sel_type = { mutable sel_path : bool}
 
-  val path_selector "model" "model_trace:TEMP_NAME": path_sel_type
+  val path_selector "model_trace:TEMP_NAME": path_sel_type
 
 end
 
@@ -14,7 +14,7 @@ module Other
 
   use import Main
 
-  let f (a : int) 
+  let f (a : int)
     ensures {result = 5}
   =
     (* The counterexample should contain the node_id 5454 here but not 121 *)
@@ -27,4 +27,4 @@ module Other
       else
         22
 
-end
\ No newline at end of file
+end

bench/ce/if_decision_branch_CVC4,1.5.oracle

@@ -4,23 +4,22 @@ Line 17:
 a, ["model_trace:a"] = {"type" : "Integer" ,
 "val" : "5" }
 Line 18:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : true }
 Line 21:
-TEMP_NAME, ["model", "node_id=5454",
+TEMP_NAME, ["node_id=5454",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 Line 25:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : true }
 
 bench/ce/if_decision_branch.mlw Other WP_parameter f : Unknown (other)
 Counter-example model:File if_decision_branch.mlw:
 Line 8:
-TEMP_NAME.sel_path, ["model",
-"model_trace:TEMP_NAME.sel_path"] = {"type" : "Boolean" ,
+TEMP_NAME.sel_path, ["model_trace:TEMP_NAME.sel_path"] = {"type" : "Boolean" ,
 "val" : false }
 Line 17:
 a, ["model_trace:a"] = {"type" : "Integer" ,
@@ -28,11 +27,11 @@ a, ["model_trace:a"] = {"type" : "Integer" ,
 Line 18:
 the check fails with all inputs
 Line 21:
-TEMP_NAME, ["model", "node_id=5454",
+TEMP_NAME, ["node_id=5454",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 Line 25:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : true }
 

bench/ce/if_decision_branch_Z3,4.6.0.oracle

@@ -4,15 +4,15 @@ Line 17:
 a, ["model_trace:a"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 18:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 Line 21:
-TEMP_NAME, ["model", "node_id=5454",
+TEMP_NAME, ["node_id=5454",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 Line 25:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 
@@ -24,11 +24,11 @@ a, ["model_trace:a"] = {"type" : "Integer" ,
 Line 18:
 the check fails with all inputs
 Line 21:
-TEMP_NAME, ["model", "node_id=5454",
+TEMP_NAME, ["node_id=5454",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 Line 25:
-TEMP_NAME, ["model", "node_id=121",
+TEMP_NAME, ["node_id=121",
 "model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
 "val" : false }
 

bench/ce/int.mlw

@@ -11,7 +11,7 @@ theory T
 
   goal g2_lab : forall x:int. (g >= x)
 
-  goal newgoal : forall x1 "model" "model_trace:X" x2 x3 x4 x5 x6 x7 x8.
+  goal newgoal : forall x1 "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

@@ -19,7 +19,7 @@ x, ["model_trace:x"] = {"type" : "Integer" ,
 bench/ce/int.mlw T newgoal : Unknown (other)
 Counter-example model:File int.mlw:
 Line 14:
-X, ["model", "model_trace:X"] = {"type" : "Integer" ,
+X, ["model_trace:X"] = {"type" : "Integer" ,
 "val" : "1" }
 x2, ["model_trace:x2"] = {"type" : "Integer" ,
 "val" : "1" }
@@ -57,7 +57,7 @@ x, ["model_trace:x"] = {"type" : "Integer" ,
 bench/ce/int.mlw T newgoal : Unknown (other)
 Counter-example model:File int.mlw:
 Line 14:
-X, ["model", "model_trace:X"] = {"type" : "Integer" ,
+X, ["model_trace:X"] = {"type" : "Integer" ,
 "val" : "1" }
 x2, ["model_trace:x2"] = {"type" : "Integer" ,
 "val" : "1" }

bench/ce/int_Z3,4.6.0.oracle

@@ -19,7 +19,7 @@ x, ["model_trace:x"] = {"type" : "Integer" ,
 bench/ce/int.mlw T newgoal : Unknown (other)
 Counter-example model:File int.mlw:
 Line 14:
-X, ["model", "model_trace:X"] = {"type" : "Integer" ,
+X, ["model_trace:X"] = {"type" : "Integer" ,
 "val" : "1" }
 x2, ["model_trace:x2"] = {"type" : "Integer" ,
 "val" : "1" }
@@ -57,7 +57,7 @@ x, ["model_trace:x"] = {"type" : "Integer" ,
 bench/ce/int.mlw T newgoal : Unknown (other)
 Counter-example model:File int.mlw:
 Line 14:
-X, ["model", "model_trace:X"] = {"type" : "Integer" ,
+X, ["model_trace:X"] = {"type" : "Integer" ,
 "val" : "1" }
 x2, ["model_trace:x2"] = {"type" : "Integer" ,
 "val" : "1" }

tests/demo-itp.mlw

@@ -15,31 +15,31 @@ module ApplyRewrite
   axiom H: forall x. (\z: int. x + z) =  f x
 
   goal g1: (\toto. 42 + toto) = f 42
-  
+
   axiom Ha: forall x. (\z: int. x + z) 2 = 2
-  
-  goal g3: (\toto. 42 + toto) 2 = 2 
-    
+
+  goal g3: (\toto. 42 + toto) 2 = 2
+
   goal g2: (\y. y + y) = f 24
 end
 
 module A
-  
+
   use import int.Int
   use HighOrd
 
   function f int: int
 
   axiom H: forall y. exists x. f x = x + y
-  
+
   goal g1: exists x. f x = x + 42
-  
+
   goal g: (\y. f y) 0 = 3
 
   constant b: bool
 
   axiom Ha: forall y. if b = true then let x = 3 in f x = x + y else false
-  
+
   goal ga: if b = true then let z = 3 in f z = z + 42 else false
 
   goal gb: if b  = true then let z = 453 in f z = z + 42 else false
@@ -61,9 +61,9 @@ end
 module TestCEX
 
   use import int.Int
-  
-  goal g: forall x "model". x=0
-  
+
+  goal g: forall x. x=0
+
 end
 
 module TestCopyPaste