search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Dumping of const arrays is incorrect #83

Closed dbueno closed 4 years ago

dbueno commented 4 years ago

I believe this condition is wrong: https://github.com/Boolector/boolector/blob/master/src/dumper/btordumpsmt.c#L806

Instead it should look like this:

          if (btor_node_is_update (real_exp->e[0])
              || btor_node_is_uf_array (real_exp->e[0])
              || btor_node_is_const_array (real_exp->e[0]))

Currently, when there is a select from const array, Boolector prints this as if it were a function call to the array, instead of a call to "select." Boolector actually parses this fine (so does yices), but Z3 chokes.

mpreiner commented 4 years ago

Thanks and fixed!