force sorting of AC_CONFIG_FILES, otherwise different computers generate the configur...

diff --git a/configure b/configure
index 24bd90127f10f563ca84b1fb3fc73c6578a0f6fc..7fdf9bb396b980c53f5949198a8329e7f04558df 100755 (executable)
--- a/configure
+++ b/configure
@@ -16462,7 +16462,7 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 mk_include=include
 
 
-ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/util/Makefile src/expr/Makefile src/theory/bool/Makefile src/theory/uf/Makefile src/theory/arith/Makefile src/theory/Makefile src/context/Makefile src/parser/cvc/Makefile src/parser/Makefile src/parser/smt/Makefile src/prop/Makefile src/prop/minisat/Makefile src/main/Makefile src/Makefile src/smt/Makefile test/unit/Makefile test/system/Makefile test/Makefile test/regress/regress3/Makefile test/regress/Makefile test/regress/regress0/Makefile test/regress/regress2/Makefile test/regress/regress1/Makefile"
+ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/context/Makefile src/expr/Makefile src/main/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/prop/Makefile src/prop/minisat/Makefile src/smt/Makefile src/theory/Makefile src/theory/arith/Makefile src/theory/bool/Makefile src/theory/uf/Makefile src/util/Makefile test/Makefile test/regress/Makefile test/regress/regress0/Makefile test/regress/regress1/Makefile test/regress/regress2/Makefile test/regress/regress3/Makefile test/system/Makefile test/unit/Makefile"
 
 
 cat >confcache <<\_ACEOF
@@ -17546,29 +17546,29 @@ do
     "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;;
     "contrib/Makefile") CONFIG_FILES="$CONFIG_FILES contrib/Makefile" ;;
     "doc/Makefile") CONFIG_FILES="$CONFIG_FILES doc/Makefile" ;;
-    "src/util/Makefile") CONFIG_FILES="$CONFIG_FILES src/util/Makefile" ;;
-    "src/expr/Makefile") CONFIG_FILES="$CONFIG_FILES src/expr/Makefile" ;;
-    "src/theory/bool/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/bool/Makefile" ;;
-    "src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;;
-    "src/theory/arith/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/arith/Makefile" ;;
-    "src/theory/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/Makefile" ;;
+    "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;;
     "src/context/Makefile") CONFIG_FILES="$CONFIG_FILES src/context/Makefile" ;;
-    "src/parser/cvc/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/cvc/Makefile" ;;
+    "src/expr/Makefile") CONFIG_FILES="$CONFIG_FILES src/expr/Makefile" ;;
+    "src/main/Makefile") CONFIG_FILES="$CONFIG_FILES src/main/Makefile" ;;
     "src/parser/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/Makefile" ;;
+    "src/parser/cvc/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/cvc/Makefile" ;;
     "src/parser/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/smt/Makefile" ;;
     "src/prop/Makefile") CONFIG_FILES="$CONFIG_FILES src/prop/Makefile" ;;
     "src/prop/minisat/Makefile") CONFIG_FILES="$CONFIG_FILES src/prop/minisat/Makefile" ;;
-    "src/main/Makefile") CONFIG_FILES="$CONFIG_FILES src/main/Makefile" ;;
-    "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;;
     "src/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/smt/Makefile" ;;
-    "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
-    "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;;
+    "src/theory/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/Makefile" ;;
+    "src/theory/arith/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/arith/Makefile" ;;
+    "src/theory/bool/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/bool/Makefile" ;;
+    "src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;;
+    "src/util/Makefile") CONFIG_FILES="$CONFIG_FILES src/util/Makefile" ;;
     "test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;;
-    "test/regress/regress3/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress3/Makefile" ;;
     "test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;;
     "test/regress/regress0/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress0/Makefile" ;;
-    "test/regress/regress2/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress2/Makefile" ;;
     "test/regress/regress1/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress1/Makefile" ;;
+    "test/regress/regress2/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress2/Makefile" ;;
+    "test/regress/regress3/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress3/Makefile" ;;
+    "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;;
+    "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
 
   *) as_fn_error "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
   esac

diff --git a/configure.ac b/configure.ac
index abd9d6df238af6138cb059aee864e6f21053283d..7b27b8b6fd0a8934389bcfd4eb9e080044aa709b 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -424,7 +424,7 @@ AC_SUBST(mk_include)
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 )
 
 AC_OUTPUT

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 23a4c6f84a86f35e5d8209b663d33f0454f608f5..765a2f49384819fc39849e74702d7c7deb214fb4 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -86,6 +86,9 @@ class NodeBuilder {
     }
   }
 
+  // dealloc: only call this with d_used == false and evIsAllocated()
+  inline void dealloc();
+
   void crop() {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     if(EXPECT_FALSE( evIsAllocated() ) && EXPECT_TRUE( d_size > d_ev->d_nchildren )) {
@@ -474,14 +477,7 @@ inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
   if(!d_used) {
     Warning("NodeBuilder unused at destruction\n");
 
-    for(iterator i = d_ev->ev_begin();
-        i != d_ev->ev_end();
-        ++i) {
-      (*i)->dec();
-    }
-    if(evIsAllocated()) {
-      free(d_ev);
-    }
+    dealloc();
   }
 }
 
@@ -490,14 +486,7 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
   if(!d_used) {
     Warning("NodeBuilder unused at clear\n");
 
-    for(iterator i = d_ev->ev_begin();
-        i != d_ev->ev_end();
-        ++i) {
-      (*i)->dec();
-    }
-    if(evIsAllocated()) {
-      free(d_ev);
-    }
+    dealloc();
   }
 
   d_size = nchild_thresh;
@@ -552,6 +541,27 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
   }
 }
 
+template <unsigned nchild_thresh>
+inline void NodeBuilder<nchild_thresh>::dealloc() {
+  /* Prefer asserts to if() because usually these conditions have been
+   * checked already, so we don't want to do a double-check in
+   * production; these are just sanity checks for debug builds */
+  Assert(!d_used,
+         "Internal error: NodeBuilder: dealloc() called with d_used");
+  Assert(evIsAllocated(),
+         "Internal error: NodeBuilder: "
+         "dealloc() called with stack-allocated NodeBuilder");
+
+  for(iterator i = d_ev->ev_begin();
+      i != d_ev->ev_end();
+      ++i) {
+    (*i)->dec();
+  }
+  if(evIsAllocated()) {
+    free(d_ev);
+  }
+}
+
 template <unsigned nchild_thresh>
 NodeBuilder<nchild_thresh>::operator Node() {// not const
   Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
@@ -580,6 +590,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
     NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev);
     if(ev != NULL) {
       // expression already exists in node manager
+      dealloc();
       d_used = true;
       Debug("prop") << "result: " << Node(ev) << std::endl;
       return Node(ev);