1 files changed, 23 insertions, 2 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 028288dbc..24e485f5e 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,6 +1,17 @@
-configure_file(floatingpoint.h.in floatingpoint.h)
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Mathias Preiner, Gereon Kremer, Andrew Reynolds
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h)
 configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
+configure_file(real_algebraic_number.h.in real_algebraic_number.h)
 
 libcvc4_add_sources(
   abstract_value.cpp
@@ -15,6 +26,9 @@ libcvc4_add_sources(
   divisible.cpp
   divisible.h
   floatingpoint.cpp
+  floatingpoint.h
+  floatingpoint_size.cpp
+  floatingpoint_size.h
   gmp_util.h
   hash.h
   iand.h
@@ -23,7 +37,8 @@ libcvc4_add_sources(
   maybe.h
   ostream_util.cpp
   ostream_util.h
-  proof.h
+  poly_util.cpp
+  poly_util.h
   random.cpp
   random.h
   resource_manager.cpp
@@ -32,6 +47,7 @@ libcvc4_add_sources(
   result.h
   regexp.cpp
   regexp.h
+  roundingmode.h
   safe_print.cpp
   safe_print.h
   sampler.cpp
@@ -46,6 +62,7 @@ libcvc4_add_sources(
   statistics_registry.h
   string.cpp
   string.h
+  floatingpoint_literal_symfpu.cpp
   tuple.h
   unsafe_interrupt_exception.h
   utility.cpp
@@ -59,3 +76,7 @@ endif()
 if(CVC4_USE_GMP_IMP)
   libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp)
 endif()
+
+if(CVC4_USE_POLY_IMP)
+  libcvc4_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h)
+endif()