Merge branch 'master' into fixGetUnsatAssumptDumpfixGetUnsatAssumptDump

3 files changed, 5 insertions, 33 deletions

diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 1b0e88098..c6d19a3ea 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -49,7 +49,7 @@ handle_option() {
       ;;
     -*|*=*)
       ;;
-    production|production-*|debug|debug-*|competition|competition-*)
+    production|production-*|debug|debug-*|competition|competition-*|testing|testing-*)
       # regexp `\?' not supported on Mac OS X
       ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
       ac_cvc4_build_profile_set=yes
@@ -103,18 +103,7 @@ handle_option() {
 unset ac_cvc4_rewritten_args
 for ac_option
 do
-  if test "$ac_option" = personal; then
-    if test -e personal.conf; then
-      handle_option --enable-personal-make-rules
-      while read arg; do
-        handle_option "$arg"
-      done < personal.conf
-    else
-      AC_MSG_ERROR([personal build profile selected, but cannot find personal.conf])
-    fi
-  else
-    handle_option "$ac_option"
-  fi
+  handle_option "$ac_option"
 done
 eval set x $ac_cvc4_rewritten_args
 shift
diff --git a/configure.ac b/configure.ac
index f802fa1c0..3eca4da99 100644
--- a/configure.ac
+++ b/configure.ac
@@ -112,7 +112,7 @@ fi
 AC_MSG_CHECKING([for requested build profile])
 AC_ARG_WITH([build],
   [AS_HELP_STRING([--with-build=profile],
-     [for profile in {production,debug,competition,personal}])])
+     [for profile in {production,debug,competition,testing}])])
 
 if test -z "${with_build+set}"; then
   with_build=production
@@ -532,7 +532,7 @@ case "$with_build" in
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     if test -z "${enable_valgrind+set}"     ; then enable_valgrind=optional         ; fi
     ;;
-  default) # moderately optimized, assertions, tracing, dumping
+  testing) # moderately optimized, assertions, tracing, dumping
     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
@@ -579,8 +579,8 @@ if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 
 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
-AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT],     [test "$with_build" = default])
 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
+AM_CONDITIONAL([CVC4_BUILD_PROFILE_TESTING],     [test "$with_build" = testing])
 
 # permit a static binary
 AC_MSG_CHECKING([whether to build a static binary])
@@ -1012,22 +1012,6 @@ if test "$target_vendor" = apple; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
 fi
 
-# Tell top-level Makefile to include $(top_srcdir)/personal.mk
-AC_ARG_ENABLE([personal-make-rules],
-  [AS_HELP_STRING([--enable-personal-make-rules],
-     [include top-level personal.mk (if it exists)])])
-if test "$enable_personal_make_rules" = yes; then
-  # This allows us to include a personal.mk makefile from every
-  # generated makefile.  Named zz_* in order to make sure this
-  # comes last, so it gets other definitions (in particular top_srcdir).
-  zz_cvc4_use_personal_make_rules='yes
-
-all:;
-include $(top_srcdir)/personal.mk
-$(top_srcdir)/personal.mk:; @touch "$@"'
-  AC_SUBST([zz_cvc4_use_personal_make_rules])
-fi
-
 # Doxygen configuration
 AC_ARG_ENABLE([internals-documentation],
   [AS_HELP_STRING([--enable-internals-documentation],
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 90928c0bc..8cb530a62 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -73,7 +73,6 @@ private:
   //fixed finite set range
   std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range;
   std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range;
-  void hasFreeVar( Node f, Node n );
   void process( Node q, Node n, bool pol,
                 std::map< Node, unsigned >& bound_lit_type_map,
                 std::map< int, std::map< Node, Node > >& bound_lit_map,