diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-01 01:56:57 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-30 23:56:57 -0700 |
| commit | 2e1b546811778f2c95f07b70f42e458b0552fab0 (patch) | |
| tree | e819e393153d339128914477b9bbf0e458bcf4ed /test/regress/CMakeLists.txt | |
| parent | 8182ab9f7d8d6c732202371c24bafd721ef6cfcc (diff) | |
Trivial solve method for single invocation sygus (#3328)
This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b47d22492..ca33b45c5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -887,6 +887,8 @@ set(regress_0_tests regress0/sygus/array-grammar-store.sy regress0/sygus/c100.sy regress0/sygus/ccp16.lus.sy + regress0/sygus/cegqi-si-string-triv.sy + regress0/sygus/cegqi-si-string-triv-2fun.sy regress0/sygus/check-generic-red.sy regress0/sygus/const-var-test.sy regress0/sygus/dt-no-syntax.sy |