diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 14:34:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-02 14:34:38 -0500 |
commit | ef4bac5d6082c21afc43c896552290d3026ede75 (patch) | |
tree | 9db744dea40e3a253a0aeb057337076755fa62bd /test | |
parent | 12bad5f9c981dd1a328dd769176e87e39a041f91 (diff) |
Remove simplification specialized for sygus si solution reconstruction (#3147)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19e5fa899..9a1e5d6dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1635,9 +1635,7 @@ set(regress_1_tests regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy - regress1/sygus/array_search_2.sy regress1/sygus/array_search_5-Q-easy.sy - regress1/sygus/array_sum_2_5.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/car_3.lus.sy regress1/sygus/cegar1.sy @@ -1652,7 +1650,6 @@ set(regress_1_tests regress1/sygus/constant-ite-bv.sy regress1/sygus/constant.sy regress1/sygus/crci-ssb-unk.sy - regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy regress1/sygus/cube-nia.sy regress1/sygus/double.sy @@ -2176,6 +2173,10 @@ set(regression_disabled_tests regress1/sygus/Base16_1.sy regress1/sygus/enum-test.sy regress1/sygus/inv_gen_fig8.sy + # rely on heuristic solution reconstruction TODO #3146 revisit + regress1/sygus/array_search_2.sy + regress1/sygus/array_sum_2_5.sy + regress1/sygus/crcy-si-rcons.sy regress2/arith/arith-int-098.cvc regress2/arith/miplib-opt1217--27.smt2 regress2/arith/miplib-pp08a-3000.smt2 |