Commit 00f86a8c authored by David Hauzar's avatar David Hauzar

A test for testing generating counterexamples.

parent 9381e853
......@@ -12,6 +12,16 @@ theory T
goal g2_lab : forall x "model":int. ("model" g >= x)
goal newgoal : forall x1 "model" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
("model" x1 + 1 = 2) ->
("model" x2 + 1 = 2) ->
("model" x3 + 1 = 2) ->
("model" x4 + 1 = 2) ->
("model" x5 + 1 = 2) ->
("model" x6 + 1 = 2) ->
("model" x7 + 1 = 2) ->
("model" x8 + 1 = 2) ->
("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
......
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