Open zqzqz opened 4 years ago
Sally does not support quantifiers at the moment.
Most SMT solvers we work with do not support quantifiers (Yices2, MathSAT, OpenSMT) and we try to stay in decidable quantifier-free fragments. If there was an appealing use-case we could add support through Z3 but this could only be used for BMC and k-induction.
Does Sally support exists and forall operators? I tried a simple example but it throws parser error at the location of "exists".