diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/cube-nia.sy | 27 |
2 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fb0e358e2..0b4a4bdc7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1603,6 +1603,7 @@ set(regress_1_tests regress1/sygus/crci-ssb-unk.sy regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy + regress1/sygus/cube-nia.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy regress1/sygus/fg_polynomial3.sy diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy new file mode 100644 index 000000000..da7d98e66 --- /dev/null +++ b/test/regress/regress1/sygus/cube-nia.sy @@ -0,0 +1,27 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic NIA) + +(synth-fun cube ((x Int)) Int + ( + (Start Int (ntInt)) + + (ntBool Bool + ( + (> ntInt ntInt) + (= ntInt ntInt) + ) + ) + (ntInt Int + (1 x + (* ntInt ntInt) + (ite ntBool ntInt ntInt) + ) + ) + ) +) + +(constraint (= (cube 1) 1)) +(constraint (= (cube 2) 8)) +(check-synth) |