diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-18 22:51:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-18 22:51:50 -0700 |
| commit | e8884b9b8ba86ce71807887cab87a5188cce4003 (patch) | |
| tree | 3b56553ecc3227eafe7aca057c5e29cd8efb63e0 /test/regress/CMakeLists.txt | |
| parent | 3054cd99db968eb85a9195b12e17e83a334e00cb (diff) | |
Add logic check for define-fun(s)-rec (#4577)
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at
the level of the new API that checks whether the logic is quantified and
includes UF. To make sure that the parser actually executes that check,
this commit converts the `DefineFunctionRecCommand` command to use the
new API instead of the old one. This temporarily breaks the `exportTo`
functionality for `DefineFunctionRecCommand` but this is not currently
used within the CVC4 code base (and it seems unlikely that users use
commands).
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cdac5fc6c..5ae66f203 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -920,6 +920,7 @@ set(regress_0_tests regress0/simplification_bug2.smtv1.smt2 regress0/smallcnf.cvc regress0/smt2output.smt2 + regress0/smtlib/define-fun-rec-logic.smt2 regress0/smtlib/get-unsat-assumptions.smt2 regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 |