False typechecker error (expected: Unknown)
Opened this issue · 0 comments
jiwonparc commented
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.