In reply to Naveenkb:
Chaining implication operators does not work the way you think it does. Two things to remember are
-
Implication is a Boolean operator: {a → c} is equivalent to {!a || c}
-
Associatively is right to left: {a → c → d} is equivalent to {a → {c → d}}
So your constraint (ignoring the foreach)
a == 0 -> c == 0 -> d == 0 -> {e.size == 5}
is equivalent to
a != 0 || c != 0 || d != 0 || e.size == 5
So a=0, c=0, d=1 becomes a valid solution, then the size of e is unconstrained.
I think your intent is
a == 0 && c == 0 -> {d == 0; e.size == 5; foreach (e[i]) e[i] inside{[1:5]};}
a == 0 && c == 1 -> {d == 1; e.size == 10; foreach (e[i]) e[i] inside{[6:10]};}
a == 1 && c == 0 -> {d == 2; e.size == 15; foreach (e[i]) e[i] inside{[11:15]};}
a == 1 && c == 1 -> {d == 3; e.size == 20; foreach (e[i]) e[i] inside{[15:20]};}