3 files changed, 33 insertions, 15 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index fd770e9f9..ca2b19a96 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -22,6 +22,7 @@ TESTS =	\
 	eq_diamond23.smt \
 	NEQ016_size5_reduced2a.smt \
 	NEQ016_size5_reduced2b.smt \
+	ccredesign-fuzz.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
 	gensys_brn001.smt2 \
@@ -31,7 +32,6 @@ TESTS =	\
 	simple.04.cvc
 
 EXTRA_DIST = $(TESTS) \
-	euf_simp09.tim.smt \
 	mkpidgeon
 
 #if CVC4_BUILD_PROFILE_COMPETITION
diff --git a/test/regress/regress0/uf/ccredesign-fuzz.smt b/test/regress/regress0/uf/ccredesign-fuzz.smt
new file mode 100644
index 000000000..d7a658600
--- /dev/null
+++ b/test/regress/regress0/uf/ccredesign-fuzz.smt
@@ -0,0 +1,32 @@
+(benchmark fuzzsmt
+:logic QF_UF
+:status sat
+:extrasorts (S1)
+:extrasorts (S0)
+:extrafuns ((v0 S0))
+:extrafuns ((v1 S0))
+:extrafuns ((f4 S1 S1))
+:extrafuns ((v2 S1))
+:extrafuns ((v3 S1))
+:extrapreds ((p3 S0 S0 S1))
+:extrafuns ((f0 S0 S0 S1 S0))
+:extrapreds ((p1 S0 S1 S1))
+:extrapreds ((p4 S1))
+:formula
+(flet ($n1 (p4 v3))
+(let (?n2 (f4 v2))
+(flet ($n3 (p4 ?n2))
+(flet ($n4 (p1 v0 ?n2 ?n2))
+(let (?n5 (f0 v1 v1 v2))
+(let (?n6 (ite $n4 ?n5 v0))
+(flet ($n7 (p3 ?n6 v0 ?n2))
+(flet ($n8 (iff $n3 $n7))
+(flet ($n9 (= v3 ?n2))
+(let (?n10 (ite $n9 v1 v0))
+(flet ($n11 (distinct ?n10 ?n10))
+(flet ($n12 false)
+(flet ($n13 (implies $n11 $n12))
+(flet ($n14 (implies $n13 $n12))
+(flet ($n15 (if_then_else $n1 $n8 $n14))
+$n15
+))))))))))))))))
diff --git a/test/regress/regress0/uf/euf_simp09.tim.smt b/test/regress/regress0/uf/euf_simp09.tim.smt
deleted file mode 100644
index 309090507..000000000
--- a/test/regress/regress0/uf/euf_simp09.tim.smt
+++ /dev/null
@@ -1,14 +0,0 @@
-% COMMAND-LINE: --uf tim
-% EXPECT: unsat
-% EXIT: 20
-(benchmark euf_simp9.smt
-
-  :status unsat
-  :difficulty { unknown }
-  :category { crafted }
-  :logic QF_UF
-  :extrasorts (A)
-  :extrafuns ((x A))
-  :extrafuns ((f A A))
-  :formula (let (?cvc_1 (f (f x))) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) x)) (= ?cvc_1 x)))))
-)