janhaag/PSE2011 — Issue #68: default value of bools in SMTLibTranslator wrong
Author: ratefuchs
Created: 2012-02-28 22:25:33+00:00
State: open
Labels: Verifier/SMTLib

Translation of the following program does not work as expected:
main(){bool i;}ensure i;

The test case fails:
Expected :(set-logic AUFNIRA)(push)(assert (not (and true (and false true))))(check-sat)(get-model)(pop)
Actual :(set-logic AUFNIRA)(push)(assert (not (and true (and true true))))(check-sat)(get-model)(pop)

The problem is that the STMLibTranslator takes the default value of Bools as "true", not as "false" like it is expected.