From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 12 Jun 2012 19:21:30 +0000 (+0000)
Subject: Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification
X-Git-Tag: cvc5-1.0.0~8060
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a450fbb38547d42fe618b325b06a4aff430dd378;p=cvc5.git

Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification
---

diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt
new file mode 100644
index 000000000..23e4ba01f
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt
@@ -0,0 +1,18 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((select_format Int Int))
+:extrafuns ((adr_lo Int))
+:extrafuns ((arg1 Int))
+:status unknown
+:formula
+(let (?n1 (select_format arg1))
+(flet ($n2 (= ?n1 adr_lo))
+(let (?n3 0)
+(flet ($n4 (= adr_lo ?n3))
+(let (?n5 1)
+(let (?n6 (select_format ?n5))
+(flet ($n7 (= adr_lo ?n6))
+(flet ($n8 (or $n4 $n7))
+(flet ($n9 (and $n2 $n8))
+$n9
+))))))))))