Consider the following Boogie program
assume sin == 0;
assert sin >= 0;
Boogie doesn't sanitize variable names used in SMTLIBv2 query passed to the solver so
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 220.127.116.11016, 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.