janhaag/PSE2011 — Issue #82: z3 grammar cannot parse all quantified expression results correctly
Author: ratefuchs
Created: 2012-03-03 20:06:35+00:00
State: open
Labels: Verifier/SMTLib

When proving the following program:

main(){}ensure exists x() forall y() x==y;

the confusing result message "false; [1]=1" is shown on verifier console.
IDE console yields an error message:
line 6:19 mismatched input '!' expecting '('

The result given by Z3 is correct SMTLib code:

sat
(model
(define-fun k!5 ((x!1 Int)) Int
(ite (= x!1 1) 1
0))
(define-fun y$2!0!6 ((x!1 Int)) Int
(ite (= x!1 1) 2
1))
(define-fun y$2!0 ((x!1 Int)) Int
(y$2!0!6 (k!5 x!1)))
)