Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre for the...
authorMorgan Deters <mdeters@cs.nyu.edu>
Wed, 2 Jul 2014 20:22:13 +0000 (16:22 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sun, 13 Jul 2014 00:49:47 +0000 (20:49 -0400)
commit5d736412de07fc555130746fc58a9224d0891105
tree7b8e755444ba0f30187e04790a0fff692b52eb22
parent4f3c678ba0b74bfe73472c6ba068e2bf712d1bb9
Fix a bug in Boolean terms and arrays.  Thanks to Jean-Christophe Filliatre for the report.
src/options/Makefile.am
src/smt/boolean_terms.cpp
src/smt/smt_engine.cpp
src/theory/arrays/kinds
src/theory/arrays/theory_arrays_type_rules.h
test/regress/regress0/Makefile.am
test/regress/regress0/boolean-terms-bug-array.smt2 [new file with mode: 0644]