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.

1 files changed, 23 insertions, 0 deletions

diff --git a/test/regress/regress0/bug303.smt2 b/test/regress/regress0/bug303.smt2
new file mode 100644
index 000000000..bf603bc62
--- /dev/null
+++ b/test/regress/regress0/bug303.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_LIA)
+(set-info :status unsat)
+
+;; don't use a datatypes for currently focusing in uf
+(declare-sort list 0)
+
+(declare-fun cons (Int list) list)
+(declare-fun nil () list)
+
+;;define length
+(declare-fun length (list) Int)
+
+(assert (= (length nil) 0))
+
+(declare-fun one_cons (list) list)
+
+(assert (= (length (cons 1 nil)) (+ 1 (length nil))))
+(assert (= (one_cons nil) (cons 1 nil)))
+(assert (not (= (length (one_cons nil)) 1)))
+
+(check-sat)
+
+(exit)