testsmt/yinyang

False typechecker error (expected: Unknown)

Opened this issue · 0 comments

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.