From 64cef995a521ac7211b9e3ed95c85deb186ff352 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Oct 2019 18:15:28 -0500 Subject: Fixes for SyGuS + regular expressions (#3313) This commit fixes numerous issues involving the combination of SyGuS and regular expressions. Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior. --- test/regress/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) (limited to 'test/regress/CMakeLists.txt') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 876751b02..8fc4b6410 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1728,6 +1728,7 @@ set(regress_1_tests regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy + regress1/sygus/re-concat.sy regress1/sygus/repair-const-rl.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy -- cgit v1.2.3