From 0d310d6716d1ab679cd466a2e47e5c0f6cdd8569 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 8 Oct 2018 19:44:22 -0700 Subject: BV instantiator: Factor out util functions. (#2604) Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this. --- src/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f6c66b743..0ea7a6837 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -434,6 +434,8 @@ libcvc4_add_sources( theory/quantifiers/cegqi/ceg_arith_instantiator.h theory/quantifiers/cegqi/ceg_bv_instantiator.cpp theory/quantifiers/cegqi/ceg_bv_instantiator.h + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h theory/quantifiers/cegqi/ceg_dt_instantiator.cpp theory/quantifiers/cegqi/ceg_dt_instantiator.h theory/quantifiers/cegqi/ceg_epr_instantiator.cpp -- cgit v1.2.3