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.

2 files changed, 25 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 0bc78e6c4..6947ea7c4 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -94,7 +94,8 @@ BUG_TESTS = \
 	bug187.smt2 \
 	bug220.smt2 \
 	bug239.smt \
-	buggy-ite.smt2
+	buggy-ite.smt2 \
+	bug303.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
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)