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.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4f79758c4f144c525acadffc3b691d7331c87bb5..5632cf438a6b4afa1a68c7151de0f9e945ef10e0 100644 (file)
--- 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 (file)
index 0000000..0bd6810
--- /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)