Commit d9f2457a authored by François Bobot's avatar François Bobot

inconsistent theory : spass and z3 find it

parent d95ebb61
......@@ -165,7 +165,9 @@ theory ArrayRich
logic sub (map 'a) int int : map 'a
axiom Sub_length :
forall s : map 'a, ofs len : int. length (sub s ofs len) = len
forall s : map 'a, ofs len : int.
len >= 0 ->
length (sub s ofs len) = len
axiom Sub_get :
forall s : map 'a, ofs len i : int.
......
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