limited quantifiers in properties

[yanntm]

there is no real reason we could not use the parameters in the property specification, we having some kind of AndAll/OrAll (or forAll, forAny) quantifiers + bool expr over parameters would be nice

e.g. viking
typedef vik_t = 0..3;
property safe [reachable] : win==1 && forAll($vik : vik) { Soldier_state[$vik]==2 };

syntax to be discussed, but that forall is a boolean Expr.

[yanntm]

smt aligned "forall" and "exists" keywords for these notions seem good.

[yanntm]

(forall ($x : dom) : var[$x] == 0 || (exists ($y : dom) : $x!=$y && var[$y]==$x))

[yanntm]

commit was target bad issue number