Currently serializing from Boolector asserts a lambda model to Z3 for the memory array. The model extractor in output.ml does not handle this case well. It is currently expected that asking for bildb or gdb output will crash when using Boolector.
It is at least a bit confusing how extract a first order model from the lambda term in the general case.
My suggestion: Walk the AST looking for bitvector literals. Use Z3.Model.eval to evaluate the lambda term applied to these values. Find one fresh value in the domain. Also eval that for the else case. This is a hack and I could probably get cases where it would evaluate incorrectly.
Currently serializing from Boolector asserts a lambda model to Z3 for the memory array. The model extractor in output.ml does not handle this case well. It is currently expected that asking for bildb or gdb output will crash when using Boolector.
It is at least a bit confusing how extract a first order model from the lambda term in the general case.
My suggestion: Walk the AST looking for bitvector literals. Use Z3.Model.eval to evaluate the lambda term applied to these values. Find one fresh value in the domain. Also eval that for the
elsecase. This is a hack and I could probably get cases where it would evaluate incorrectly.