Commit 4527de9c authored by MARCHE Claude's avatar MARCHE Claude

counterexamples: extended test file on maps

There is no CE for the new module OtherIndices, but it should
parent c31bab2f
...@@ -42,3 +42,11 @@ goal t1 : forall t:map int int, i : int. ...@@ -42,3 +42,11 @@ goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i get (set t 0 42) i = get t i
end end
module OtherIndices
use map.Map
goal g : forall m: map real real. m 0.1 = 0.0 \/ m 0.2 = m 0.1
end
\ No newline at end of file
...@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" , ...@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" , {"others" : {"type" : "Integer" ,
"val" : "0" } }] } "val" : "0" } }] }
bench/ce/map.mlw OtherIndices g: Unknown (sat)
...@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" , ...@@ -174,3 +174,4 @@ t, [[@introduced]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" , {"others" : {"type" : "Integer" ,
"val" : "0" } }] } "val" : "0" } }] }
bench/ce/map.mlw OtherIndices g: Unknown (sat)
...@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" , ...@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" , {"others" : {"type" : "Integer" ,
"val" : "1" } }] } "val" : "1" } }] }
bench/ce/map.mlw OtherIndices g: Unknown (sat)
...@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" , ...@@ -195,3 +195,4 @@ t, [[@introduced]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" , {"others" : {"type" : "Integer" ,
"val" : "1" } }] } "val" : "1" } }] }
bench/ce/map.mlw OtherIndices g: Unknown (sat)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment