janhaag/PSE2011 — Issue #112: Use Z3 to evaluate unbounded quantified expressions in interpreter
Author: ratefuchs
Created: 2012-03-07 19:14:09+00:00
State: open
Labels: Feature, Interpreter, Verifier/SMTLib

Trying to interpret
main(){}ensure forall x() true;

now leads to the message that it cannot be evaluated by the interpreter.

It would be nice if those expressions are given to Z3 to be evaluated.