team-worthwhile/worthwhile — Issue #64: SMTLIB error: unknown constant
Author: jspam
Created: 2012-02-17 19:24:00+00:00
State: open
Labels: prover

[Test program and generated formula here](https://gist.github.com/1854970)

When trying to prove the program, the following error message is displayed:

```
Additional prover output: (error "line 40 column 20: unknown constant")
```

Z3 complains about ```currentCharacter``` being used (but not declared?)