diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-03 11:40:44 -0500 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-03 11:40:44 -0500 |
| commit | bc4b21307a4b63de2e2c47a4f1fa4367b9320f57 (patch) | |
| tree | 1c4fdcbeed0c104e1117a5ad3036deeaf13e1a40 /test | |
| parent | b1fe934c551dd89f1001ca2c56a146231c1e49a0 (diff) | |
Eliminate partial operators within lambdas during grammar normalization (#2570)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/multi-udiv.sy | 42 |
3 files changed, 44 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c798af378..bec5362e5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1718,6 +1718,7 @@ set(regress_2_tests regress2/sygus/lustre-real.sy regress2/sygus/max2-univ.sy regress2/sygus/mpg_guard1-dd.sy + regress2/sygus/multi-udiv.sy regress2/sygus/nia-max-square.sy regress2/sygus/no-syntax-test-no-si.sy regress2/sygus/process-10-vars-2fun.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index deb4ad647..37c911d41 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1711,6 +1711,7 @@ REG2_TESTS = \ regress2/sygus/lustre-real.sy \ regress2/sygus/max2-univ.sy \ regress2/sygus/mpg_guard1-dd.sy \ + regress2/sygus/multi-udiv.sy \ regress2/sygus/nia-max-square.sy \ regress2/sygus/no-syntax-test-no-si.sy \ regress2/sygus/process-10-vars-2fun.sy \ diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy new file mode 100644 index 000000000..657417595 --- /dev/null +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -0,0 +1,42 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + ( set-logic BV ) + ( define-fun hd05 ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( bvor x ( bvsub x #x00000001 ) ) ) +( synth-fun f ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( + (Start ( BitVec 32 ) ( #x00000001 + #x00000000 + #xffffffff + x + (bvsrem NT0 NT0) + (bvudiv NT0 NT0) + (bvsdiv NT0 NT0) + (bvurem NT0 NT0) + (bvsrem NT4 NT0) + (bvudiv NT4 NT0) + (bvurem NT4 NT0) + (bvsdiv NT4 NT0) + (bvnot NT0) + (bvneg NT0) + (bvadd NT0 NT0) + (bvor NT0 NT0) + (bvor NT4 NT0) + (bvadd NT4 NT0) +)) + (NT0 ( BitVec 32 ) ( #x00000001 + #x00000000 + #xffffffff + x +)) + (NT4 ( BitVec 32 ) ( (bvnot NT0) + (bvneg NT0) + (bvadd NT0 NT0) + (bvor NT0 NT0) + (bvsrem NT0 NT0) + (bvudiv NT0 NT0) + (bvsdiv NT0 NT0) + (bvurem NT0 NT0) +)) +)) + ( declare-var x ( BitVec 32 ) ) + ( constraint ( = ( hd05 x ) ( f x ) ) ) + ( check-synth ) |