From e8884b9b8ba86ce71807887cab87a5188cce4003 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 18 Jun 2020 22:51:50 -0700 Subject: 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). --- 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 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 -- cgit v1.2.3