diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 6878c4af344..0fc1707f39f 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1324,6 +1324,7 @@ set(regress_0_tests
   regress0/proofs/dd_ic_pf_764.smt2
   regress0/proofs/dd_pf_739.smt2
   regress0/proofs/dd_spark_nnf_pf.smt2
+  regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2
   regress0/proofs/define-fun-shadow.smt2
   regress0/proofs/dsl-cong-eval-cr.smt2
   regress0/proofs/dsl-no-eval.smt2
diff --git a/test/regress/cli/regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2 b/test/regress/cli/regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2
new file mode 100644
index 00000000000..423642ca9f9
--- /dev/null
+++ b/test/regress/cli/regress0/proofs/dd_textbook-sumeven-arith-rcons.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun t () Int)
+(declare-fun s (Int Int Int) Int)
+(declare-fun s (Int Int Int Int Int) Int)
+(declare-fun _1 (Int Int) Int)
+(assert (and (forall ((x Int) (? Int)) (! (= 0 (_1 1 x)) :pattern ((s 0 0 x 0 ?)))) (forall ((? Int) (y Int)) (! (= (_1 0 0) (- ? (* y (_1 ? 0)))) :pattern ((_1 ? y)) :pattern ((_1 0 0))))))
+(assert (and (= 0 (_1 t 1)) (= 0 (s 0 0 2 0 (s 0 0 0)))))
+(check-sat)