Manuals/calci/THEREEXISTSONE

Description

• THEREEXISTSONE returns the result of applying the set of SomeFunctions to SomeArray, if results evaluate to true for one exactly element in the array when the functions are applied.

Example

THEREEXISTSONE(1..100,"x<=1")

gives true

THEREEXISTSONE(1..100,"x<=2")

gives false

See Also

• FORALL
• THEREEXISTS
• THEREDOESNOTEXIST
• FORDOFFUNCTIONS

References

• List of Main Z Functions

• Z3 home