Fixes for two bugs:
authorMorgan Deters <mdeters@cs.nyu.edu>
Mon, 1 Apr 2013 21:34:27 +0000 (17:34 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Tue, 2 Apr 2013 00:09:21 +0000 (20:09 -0400)
commit4d7cff8156c2e409be209f1ee489dcf05f922d50
treeb0b7ba4e98cee86b3c37094c90c980c0042db475
parenta197d41f1945dcaf64cc80fff5ac3a828c0ba0d2
Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.
src/smt/model_postprocessor.cpp
src/theory/model.cpp
test/regress/regress0/auflia/Makefile.am
test/regress/regress0/auflia/fuzz-error232.smt [new file with mode: 0644]
test/regress/regress0/datatypes/Makefile.am