1

Closed

Boogie needs to sanitize variable names used in SMTLIB output

description

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 2.3.0.61016, 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 7:17 PM by danliew
Fixed in 89d67f97b5db

comments

danliew wrote Feb 18, 2015 at 7:17 PM

Fixed in 89d67f97b5db