From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 11 Jan 2022 06:36:20 +0000 (-0600)
Subject: Check the synthesized funs of `check-synth-next`. (#7915)
X-Git-Tag: cvc5-1.0.0~570
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c2d24457f61770601308e37294316d72c595229;p=cvc5.git

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 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)