Debug prover errors generated by boogie

[rahxephon89]

When I am using Boogie 3.0.9 on Mac OS to verify a boogie program, I got an error: Prover error: line 247 column 112: unknown constant is- ((Array Int |T@$123_M_A'u64'|) |T@$123_M_A'u64'|). However, I cannot find this constant in the smt file generated by the option -proverLog:@[email protected]. Could anyone give me some hints on how to debug this issue?

This is the boogie command:
boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -proverOpt:O:model_validate=true -prov erOpt:PROVER_PATH=../bin/z3 -useArrayAxioms -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -vcsCores:1 output.bpl -proverLog:@[email protected]

The bpl and smt files are attached. Thanks!
123_M_foo_verify.smt.txt
output.bpl.txt

[atomb]

There are two things going on, I think.

• When using the declare-datatypes command in SMT-Lib, the solver synthesizes appropriate is- predicates to check whether a value is an instance of a specific alternative. You don't find the name in the file because it should be auto-generated.
• Boogie is somehow expecting to find an is- predicate for an array type rather than a datatype. And somehow the name of that type starts with a space. This seems like a bug in Boogie.

[atomb]

It also seems like a resolved bug in Boogie. Using Boogie 3.2.4, verification succeeds.

[rahxephon89]

Thanks @atomb!