* Fix some regressions' expected outputs.
authorMorgan Deters <mdeters@gmail.com>
Sat, 6 Oct 2012 04:05:19 +0000 (04:05 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 6 Oct 2012 04:05:19 +0000 (04:05 +0000)
commit9b871cceb0f9c3372504f9f7b786a7c1dd7cd700
treeda76170cfa5311ce3b72b25e8e8179a4f1aa6f6c
parent04b89b1a5256a8a70df1615c9a7873a2d870fe82
* Fix some regressions' expected outputs.

* Ensure Rewriter::init() is called before ::rewrite().
  The array type enumerator recently gave us an end-run around
  ::init().  TheoryEngine no longer calls these, they're done
  via static initialization.

* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).

(this commit was certified error- and warning-free by the test-and-commit script.)
src/parser/smt2/Smt2.g
src/theory/rewriter.cpp
src/theory/rewriter.h
src/theory/theory_engine.cpp
test/regress/regress0/push-pop/bug394.smt2
test/regress/regress0/push-pop/bug396.smt2
test/unit/theory/type_enumerator_white.h