-
Notifications
You must be signed in to change notification settings - Fork 25
Open
Labels
bugSomething isn't workingSomething isn't working
Milestone
Description
This makes the typechecker fail (but z3 and cvc4 are happy with it):
(declare-fun x () Int)
(assert (=>
(= x 3)
(forall ((x Int)) (let ((?y x))
(= ?y 3)
))
))
(check-sat)The output is:
src.parsing.typechecker.TypeCheckError: Ill-typed expression
term: (= x 3)
faulty subterm: 3
expected: Unknown
actual: Int
The error disappears when the quantified and global variable have different names.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working