From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 30 Oct 2012 23:22:07 +0000 (+0000)
Subject: delta of a model-building failure case
X-Git-Tag: cvc5-1.0.0~7654
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b4c416608bda1df62e1ffe7131648a89882ddc7;p=cvc5.git

delta of a model-building failure case
---

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 57c56c01b..289569b1a 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -33,6 +33,8 @@ SMT_TESTS = \
 	pb_real_10_0200_10_29.smt \
 	incorrect2.smt \
 	incorrect1.smt \
+	incorrect1.delta01.smt \
+	incorrect1.delta02.smt 
 	error1.smt
 
 # Regression tests for SMT2 inputs
diff --git a/test/regress/regress0/uflra/incorrect1.delta02.smt b/test/regress/regress0/uflra/incorrect1.delta02.smt
new file mode 100644
index 000000000..9d9d65edc
--- /dev/null
+++ b/test/regress/regress0/uflra/incorrect1.delta02.smt
@@ -0,0 +1,14 @@
+(benchmark fuzzsmt
+:logic QF_UFLRA
+:extrafuns ((f1 Real Real Real))
+:status sat
+:formula
+(let (?n1 6)
+(let (?n2 (~ ?n1))
+(let (?n3 (/ ?n1 ?n2))
+(let (?n4 1)
+(let (?n5 (+ ?n3 ?n4))
+(let (?n6 (f1 ?n4 ?n4))
+(flet ($n7 (distinct ?n5 ?n6))
+$n7
+))))))))