Abstract Data-Type Support in Boogie

Jul 16, 2013 at 9:14 AM
Edited Jul 16, 2013 at 12:07 PM
I was wondering if the algebraic data-type support in Boogie is supposed to be working at the moment. I tried the three examples from the test suite (test/datatypes/*.bpl), but they fail for my setup (Boogie version 2.2.30705.1126, Z3 4.3.0) as well as on rise4fun (see [1]) with a prover error. I suspect that one needs to use specific versions of Boogie and Z3 that work together. Any hints which versions work would be appreciated, and I would be willing to compile the tools myself if necessary.


[1] http://rise4fun.com/Boogie/WYN
Aug 2, 2013 at 10:13 AM
For others having the same problem: Passing the command-line option /typeEncoding:m (monomorphic type encoding) allows the examples to verify.