This project is read-only.


Boogie needs to sanitize variable names used in SMTLIB output


Consider the following Boogie program
const sin:int;

procedure main()
    assume sin == 0;
    assert sin >= 0;
Boogie doesn't sanitize variable names used in SMTLIBv2 query passed to the solver so sin is used a variable name which is also an operator name for Z3 so I get errors like this
 $ Boogie.exe varCalledSin.bpl 
Boogie program verifier version, Copyright (c) 2003-2014, Microsoft.
Prover error: line 30 column 23: invalid declaration, builtin symbol sin
Prover error: line 36 column 68: no arguments supplied to arithmetical operator
Prover error: Unexpected prover response getting labels: labels
Boogie should sanitize the variable names used in the query.
Closed Feb 18, 2015 at 8:17 PM by danliew
Fixed in 89d67f97b5db


danliew wrote Feb 18, 2015 at 8:17 PM

Fixed in 89d67f97b5db