From 3c2d24457f61770601308e37294316d72c595229 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 11 Jan 2022 00:36:20 -0600
Subject: [PATCH] Check the synthesized funs of `check-synth-next`. (#7915)

This PR ensures that the functions synthesized by cvc5 with check-synth-next command(s) are different from the preceding ones.
---
 test/regress/CMakeLists.txt                     |  1 +
 .../regress1/sygus/incremental-stream-ex2.sy    | 17 +++++++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 test/regress/regress1/sygus/incremental-stream-ex2.sy

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4f79758c4..5632cf438 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2494,6 +2494,7 @@ set(regress_1_tests
   regress1/sygus/icfp_28_10.sy
   regress1/sygus/icfp_easy-ite.sy
   regress1/sygus/incremental-stream-ex.sy
+  regress1/sygus/incremental-stream-ex2.sy
   regress1/sygus/int-any-const.sy
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
diff --git a/test/regress/regress1/sygus/incremental-stream-ex2.sy b/test/regress/regress1/sygus/incremental-stream-ex2.sy
new file mode 100644
index 000000000..0bd681036
--- /dev/null
+++ b/test/regress/regress1/sygus/incremental-stream-ex2.sy
@@ -0,0 +1,17 @@
+; COMMAND-LINE: -i
+; SCRUBBER: grep "define-fun" | sort
+; EXPECT: (define-fun f ((x Int) (y Int)) Int 0)
+; EXPECT: (define-fun f ((x Int) (y Int)) Int 1)
+; EXPECT: (define-fun f ((x Int) (y Int)) Int x)
+; EXPECT: (define-fun f ((x Int) (y Int)) Int y)
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int))
+  ((Start Int (0 1 x y))))
+
+(check-synth)
+(check-synth-next)
+(check-synth-next)
+(check-synth-next)
-- 
2.30.2