Fix for bug303. The problem was with function applications that get normalized when...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 21 Feb 2012 19:43:46 +0000 (19:43 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 21 Feb 2012 19:43:46 +0000 (19:43 +0000)
commitf52bee51e20b0670f9a2bd13ae2fdefd5eba1546
treee77af4a3fd4bd726d1f9ed1215fccf5aad1c50f2
parent9dcfc2fdc58bf46a434f9c228a828be8d580f529
Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.

Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/equality_engine_impl.h
test/regress/regress0/Makefile.am
test/regress/regress0/bug303.smt2 [new file with mode: 0644]