14 files changed, 303 insertions, 78 deletions

diff --git a/Makefile.common b/Makefile.common
index 268de9f8..d3fd1e76 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -5,6 +5,10 @@ include $(LEVEL)/Makefile.config
 # Include LLVM's Master Makefile config and rules.
 include $(LLVM_OBJ_ROOT)/Makefile.config
 
+# Assertions should be enabled by default for KLEE (but they can still
+# be disabled by running make with DISABLE_ASSERTIONS=1
+DISABLE_ASSERTIONS := 0
+
 BUILDING_RUNTIME:=$(if $(or $(BYTECODE_LIBRARY),$(MODULE_NAME)),1,0)
 ifeq ($(BUILDING_RUNTIME),1)
 #
@@ -12,7 +16,6 @@ ifeq ($(BUILDING_RUNTIME),1)
 # to override whatever the user may have said on the command line,
 # hence the use of override.
 #
-
 override ENABLE_OPTIMIZED := $(RUNTIME_ENABLE_OPTIMIZED)
 override DISABLE_ASSERTIONS := $(RUNTIME_DISABLE_ASSERTIONS)
 override ENABLE_PROFILING := $(RUNTIME_ENABLE_PROFILING)
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index ae497b48..b94843a3 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -1,7 +1,7 @@
 dnl **************************************************************************
 dnl * Initialize
 dnl **************************************************************************
-AC_INIT([[KLEE]],[[0.2.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]])
+AC_INIT([[KLEE]],[[1.0.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]])
 
 dnl Identify where LLVM source tree is (this is patched by
 dnl AutoRegen.sh)
diff --git a/configure b/configure
index 9e524f41..1f603063 100755
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for KLEE 0.2.0.
+# Generated by GNU Autoconf 2.69 for KLEE 1.0.0.
 #
 # Report bugs to <klee-dev@imperial.ac.uk>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='KLEE'
 PACKAGE_TARNAME='klee-'
-PACKAGE_VERSION='0.2.0'
-PACKAGE_STRING='KLEE 0.2.0'
+PACKAGE_VERSION='1.0.0'
+PACKAGE_STRING='KLEE 1.0.0'
 PACKAGE_BUGREPORT='klee-dev@imperial.ac.uk'
 PACKAGE_URL='https://klee.github.io'
 
@@ -1285,7 +1285,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures KLEE 0.2.0 to adapt to many kinds of systems.
+\`configure' configures KLEE 1.0.0 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1351,7 +1351,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of KLEE 0.2.0:";;
+     short | recursive ) echo "Configuration of KLEE 1.0.0:";;
    esac
   cat <<\_ACEOF
 
@@ -1463,7 +1463,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-KLEE configure 0.2.0
+KLEE configure 1.0.0
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2044,7 +2044,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by KLEE $as_me 0.2.0, which was
+It was created by KLEE $as_me 1.0.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -5619,7 +5619,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by KLEE $as_me 0.2.0, which was
+This file was extended by KLEE $as_me 1.0.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -5686,7 +5686,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-KLEE config.status 0.2.0
+KLEE config.status 1.0.0
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 032e5243..d0980395 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -110,6 +110,7 @@ extern "C" {
   void klee_warning(const char *message);
   void klee_warning_once(const char *message);
   void klee_prefer_cex(void *object, uintptr_t condition);
+  void klee_posix_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
 
   /* Return a possible constant value for the input expression. This
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 63df4b65..6fee5cb1 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -29,13 +29,13 @@ namespace klee {
   public:
     Assignment(bool _allowFreeValues=false) 
       : allowFreeValues(_allowFreeValues) {}
-    Assignment(std::vector<const Array*> &objects, 
+    Assignment(const std::vector<const Array*> &objects,
                std::vector< std::vector<unsigned char> > &values,
                bool _allowFreeValues=false) 
       : allowFreeValues(_allowFreeValues){
       std::vector< std::vector<unsigned char> >::iterator valIt = 
         values.begin();
-      for (std::vector<const Array*>::iterator it = objects.begin(),
+      for (std::vector<const Array*>::const_iterator it = objects.begin(),
              ie = objects.end(); it != ie; ++it) {
         const Array *os = *it;
         std::vector<unsigned char> &arr = *valIt;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1b2bc15b..49e526f5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -140,12 +140,6 @@ namespace {
 		   cl::desc("Dump test cases for all active states on exit (default=on)"));
  
   cl::opt<bool>
-  PreferCex("prefer-cex",
-            cl::init(false),
-            cl::desc("Prefer creation of tests with human readable bytes. Can also pair with klee_prefer_cex api "
-                     "to customize range. Note: option is expensive when creating lots of tests (default=false)"));
- 
-  cl::opt<bool>
   RandomizeFork("randomize-fork",
                 cl::init(false),
 		cl::desc("Randomly swap the true and false states on a fork (default=off)"));
@@ -3484,34 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   solver->setTimeout(coreSolverTimeout);
 
   ExecutionState tmp(state);
-  if (PreferCex) {
-    // When the PreferCex is enabled, go through each byte in every test case and
-    // attempt to restrict it to the constraints contained in cexPreferences.
-    // (Note: usually this means trying to make it an ASCII character (0-127)
-    // and therefore human readable. It is also possible to customize the preferred
-    // constraints.  See test/Features/PreferCex.c for an example)  While this
-    // process can be very expensive, it can also make understanding individual
-    // test cases much easier.
-    for (unsigned i = 0; i != state.symbolics.size(); ++i) {
-      const MemoryObject *mo = state.symbolics[i].first;
-      std::vector< ref<Expr> >::const_iterator pi = 
-        mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
-      for (; pi != pie; ++pi) {
-        bool mustBeTrue;
-        // Attempt to bound byte to constraints held in cexPreferences
-        bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
-                                          mustBeTrue);
-        // If it isn't possible to constrain this particular byte in the desired
-        // way (normally this would mean that the byte can't be constrained to
-        // be between 0 and 127 without making the entire constraint list UNSAT)
-        // then just continue on to the next byte.
-        if (!success) break;
-        // If the particular constraint operated on in this iteration through
-        // the loop isn't implied then add it to the list of constraints.
-        if (!mustBeTrue) tmp.addConstraint(*pi);
-      }
-      if (pi!=pie) break;
-    }
+
+  // Go through each byte in every test case and attempt to restrict
+  // it to the constraints contained in cexPreferences.  (Note:
+  // usually this means trying to make it an ASCII character (0-127)
+  // and therefore human readable. It is also possible to customize
+  // the preferred constraints.  See test/Features/PreferCex.c for
+  // an example) While this process can be very expensive, it can
+  // also make understanding individual test cases much easier.
+  for (unsigned i = 0; i != state.symbolics.size(); ++i) {
+    const MemoryObject *mo = state.symbolics[i].first;
+    std::vector< ref<Expr> >::const_iterator pi = 
+      mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
+    for (; pi != pie; ++pi) {
+      bool mustBeTrue;
+      // Attempt to bound byte to constraints held in cexPreferences
+      bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
+					mustBeTrue);
+      // If it isn't possible to constrain this particular byte in the desired
+      // way (normally this would mean that the byte can't be constrained to
+      // be between 0 and 127 without making the entire constraint list UNSAT)
+      // then just continue on to the next byte.
+      if (!success) break;
+      // If the particular constraint operated on in this iteration through
+      // the loop isn't implied then add it to the list of constraints.
+      if (!mustBeTrue) tmp.addConstraint(*pi);
+    }
+    if (pi!=pie) break;
   }
 
   std::vector< std::vector<unsigned char> > values;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f06ae4f5..52abff5f 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -22,6 +22,8 @@
 #include "Executor.h"
 #include "MemoryManager.h"
 
+#include "klee/CommandLine.h"
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Module.h"
 #else
@@ -34,6 +36,15 @@
 using namespace llvm;
 using namespace klee;
 
+namespace {
+  cl::opt<bool>
+  ReadablePosix("readable-posix-inputs",
+            cl::init(false),
+            cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. "
+                     "Note: option is expensive when creating lots of tests (default=false)"));
+}
+
+
 /// \todo Almost all of the demands in this file should be replaced
 /// with terminateState calls.
 
@@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_mark_global", handleMarkGlobal, false),
   add("klee_merge", handleMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
+  add("klee_posix_prefer_cex", handlePosixPreferCex, false),
   add("klee_print_expr", handlePrintExpr, false),
   add("klee_print_range", handlePrintRange, false),
   add("klee_set_forking", handleSetForking, false),
@@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
   if (!state.addressSpace.resolveOne(address, op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
-  bool res;
+  bool res __attribute__ ((unused));
   assert(executor.solver->mustBeTrue(state, 
                                      EqExpr::create(address, 
                                                     op.first->getBaseExpr()),
@@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
   
   bool res;
-  bool success = executor.solver->mustBeFalse(state, e, res);
+  bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res);
   assert(success && "FIXME: Unhandled solver failure");
   if (res) {
     executor.terminateStateOnError(state, 
@@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
   rl[0].first.first->cexPreferences.push_back(cond);
 }
 
+void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state,
+                                             KInstruction *target,
+                                             std::vector<ref<Expr> > &arguments) {
+  if (ReadablePosix)
+    return handlePreferCex(state, target, arguments);
+}
+
 void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
                                   KInstruction *target,
                                   std::vector<ref<Expr> > &arguments) {
@@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
-    bool success = executor.solver->getValue(state, arguments[1], value);
+    bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value);
     assert(success && "FIXME: Unhandled solver failure");
     bool res;
     success = executor.solver->mustBeTrue(state, 
@@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
 
     // FIXME: Type coercion should be done consistently somewhere.
     bool res;
-    bool success =
+    bool success __attribute__ ((unused)) =
       executor.solver->mustBeTrue(*s, 
                                   EqExpr::create(ZExtExpr::create(arguments[1],
                                                                   Context::get().getPointerWidth()),
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index d52b8fc5..2dfdde43 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -120,6 +120,7 @@ namespace klee {
     HANDLER(handleNew);
     HANDLER(handleNewArray);
     HANDLER(handlePreferCex);
+    HANDLER(handlePosixPreferCex);
     HANDLER(handlePrintExpr);
     HANDLER(handlePrintRange);
     HANDLER(handleRange);
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index df7fffc5..d51c1695 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -35,6 +35,11 @@ namespace {
                  cl::init(false));
 
   cl::opt<bool>
+  CexCacheSuperSet("cex-cache-superset",
+                 cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"),
+                 cl::init(false));
+
+  cl::opt<bool>
   CexCacheExperimental("cex-cache-exp", cl::init(false));
 
 }
@@ -124,8 +129,10 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
   if (CexCacheTryAll) {
     // Look for a satisfying assignment for a superset, which is trivially an
     // assignment for any subset.
-    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
-    
+    Assignment **lookup = 0;
+    if (CexCacheSuperSet)
+      lookup = cache.findSuperset(key, NonNullAssignment());
+
     // Otherwise, look for a subset which is unsatisfiable, see below.
     if (!lookup) 
       lookup = cache.findSubset(key, NullAssignment());
@@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
 
     // Look for a satisfying assignment for a superset, which is trivially an
     // assignment for any subset.
-    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
+    Assignment **lookup = 0;
+    if (CexCacheSuperSet)
+      lookup = cache.findSuperset(key, NonNullAssignment());
 
     // Otherwise, look for a subset which is unsatisfiable -- if the subset is
     // unsatisfiable then no additional constraints can produce a valid
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index dcaecb05..cfe1bb16 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -16,11 +16,13 @@
 #include "klee/Internal/Support/Debug.h"
 
 #include "klee/util/ExprUtil.h"
+#include "klee/util/Assignment.h"
 
 #include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <vector>
 #include <ostream>
+#include <list>
 
 using namespace klee;
 using namespace llvm;
@@ -62,6 +64,14 @@ public:
     return false;
   }
 
+  std::set<unsigned>::iterator begin(){
+    return s.begin();
+  }
+
+  std::set<unsigned>::iterator end(){
+    return s.end();
+  }
+
   void print(llvm::raw_ostream &os) const {
     bool first = true;
     os << "{";
@@ -86,13 +96,23 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
 }
 
 class IndependentElementSet {
+public:
   typedef std::map<const Array*, ::DenseSet<unsigned> > elements_ty;
-  elements_ty elements;
-  std::set<const Array*> wholeObjects;
+  elements_ty elements;                 // Represents individual elements of array accesses (arr[1])
+  std::set<const Array*> wholeObjects;  // Represents symbolically accessed arrays (arr[x])
+  std::vector<ref<Expr> > exprs;        // All expressions that are associated with this factor
+                                        // Although order doesn't matter, we use a vector to match
+                                        // the ConstraintManager constructor that will eventually
+                                        // be invoked.
 
-public:
   IndependentElementSet() {}
   IndependentElementSet(ref<Expr> e) {
+    exprs.push_back(e);
+    // Track all reads in the program.  Determines whether reads are
+    // concrete or symbolic.  If they are symbolic, "collapses" array
+    // by adding it to wholeObjects.  Otherwise, creates a mapping of
+    // the form Map<array, set<index>> which tracks which parts of the
+    // array are being accessed.
     std::vector< ref<ReadExpr> > reads;
     findReads(e, /* visitUpdates= */ true, reads);
     for (unsigned i = 0; i != reads.size(); ++i) {
@@ -106,6 +126,8 @@ public:
 
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+          // if index constant, then add to set of constraints operating
+          // on that array (actually, don't add constraint, just set index)
           ::DenseSet<unsigned> &dis = elements[array];
           dis.add((unsigned) CE->getZExtValue(32));
         } else {
@@ -119,11 +141,13 @@ public:
   }
   IndependentElementSet(const IndependentElementSet &ies) : 
     elements(ies.elements),
-    wholeObjects(ies.wholeObjects) {}    
+    wholeObjects(ies.wholeObjects),
+    exprs(ies.exprs) {}
 
   IndependentElementSet &operator=(const IndependentElementSet &ies) {
     elements = ies.elements;
     wholeObjects = ies.wholeObjects;
+    exprs = ies.exprs;
     return *this;
   }
 
@@ -160,6 +184,7 @@ public:
 
   // more efficient when this is the smaller set
   bool intersects(const IndependentElementSet &b) {
+    // If there are any symbolic arrays in our query that b accesses
     for (std::set<const Array*>::iterator it = wholeObjects.begin(), 
            ie = wholeObjects.end(); it != ie; ++it) {
       const Array *array = *it;
@@ -170,9 +195,11 @@ public:
     for (elements_ty::iterator it = elements.begin(), ie = elements.end();
          it != ie; ++it) {
       const Array *array = it->first;
+      // if the array we access is symbolic in b
       if (b.wholeObjects.count(array))
         return true;
       elements_ty::const_iterator it2 = b.elements.find(array);
+      // if any of the elements we access are also accessed by b
       if (it2 != b.elements.end()) {
         if (it->second.intersects(it2->second))
           return true;
@@ -183,6 +210,11 @@ public:
 
   // returns true iff set is changed by addition
   bool add(const IndependentElementSet &b) {
+    for(unsigned i = 0; i < b.exprs.size(); i ++){
+      ref<Expr> expr = b.exprs[i];
+      exprs.push_back(expr);
+    }
+
     bool modified = false;
     for (std::set<const Array*>::const_iterator it = b.wholeObjects.begin(), 
            ie = b.wholeObjects.end(); it != ie; ++it) {
@@ -208,6 +240,7 @@ public:
           modified = true;
           elements.insert(*it);
         } else {
+          // Now need to see if there are any (z=?)'s
           if (it2->second.add(it->second))
             modified = true;
         }
@@ -223,6 +256,60 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
   return os;
 }
 
+// Breaks down a constraint into all of it's individual pieces, returning a
+// list of IndependentElementSets or the independent factors.
+static
+void getAllIndependentConstraintsSets(const Query& query,
+                                      std::list<IndependentElementSet> * &factors){
+  ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr);
+  if (CE){
+    assert(CE && CE->isFalse() &&
+           "the expr should always be false and therefore not included in factors");
+  } else {
+    ref<Expr> neg = Expr::createIsZero(query.expr);
+    factors->push_back(IndependentElementSet(neg));
+  }
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+       ie = query.constraints.end(); it != ie; ++it)
+    // iterate through all the previously separated constraints.  Until we
+    // actually return, factors is treated as a queue of expressions to be
+    // evaluated.  If the queue property isn't maintained, then the exprs
+    // could be returned in an order different from how they came it, negatively
+    // affecting later stages.
+    factors->push_back(IndependentElementSet(*it));
+    bool doneLoop = false;
+    do {
+      doneLoop = true;
+      std::list<IndependentElementSet> * done = new std::list<IndependentElementSet>;
+      while (factors->size() > 0){
+        IndependentElementSet current = factors->front();
+        factors->pop_front();
+        // This list represents the set of factors that are separate from current.
+        // Those that are not inserted into this list (queue) intersect with current.
+	std::list<IndependentElementSet> *keep = new std::list<IndependentElementSet>;
+	while (factors->size() > 0){
+          IndependentElementSet compare = factors->front();
+          factors->pop_front();
+          if (current.intersects(compare)){
+            if (current.add(compare)){
+	      // Means that we have added (z=y)added to (x=y)
+	      // Now need to see if there are any (z=?)'s
+	      doneLoop = false;
+	    }
+	  } else {
+            keep->push_back(compare);
+	  }
+	}
+	done->push_back(current);
+	delete factors;
+	factors = keep;
+      }
+    delete factors;
+    factors = done;
+  } while (!doneLoop);
+}
+
 static 
 IndependentElementSet getIndependentConstraints(const Query& query,
                                                 std::vector< ref<Expr> > &result) {
@@ -244,6 +331,8 @@ IndependentElementSet getIndependentConstraints(const Query& query,
         if (eltsClosure.add(it->second))
           done = false;
         result.push_back(it->first);
+        // Means that we have added (z=y)added to (x=y)
+        // Now need to see if there are any (z=?)'s
       } else {
         newWorklist.push_back(*it);
       }
@@ -270,6 +359,27 @@ IndependentElementSet getIndependentConstraints(const Query& query,
   return eltsClosure;
 }
 
+
+// Extracts which arrays are referenced from a particular independent set.  Examines both
+// the actual known array accesses arr[1] plus the undetermined accesses arr[x].
+static
+void calculateArrayReferences(const IndependentElementSet & ie,
+                              std::vector<const Array *> &returnVector){
+  std::set<const Array*> thisSeen;
+  for(std::map<const Array*, ::DenseSet<unsigned> >::const_iterator it = ie.elements.begin();
+      it != ie.elements.end(); it ++){
+    thisSeen.insert(it->first);
+  }
+  for(std::set<const Array *>::iterator it = ie.wholeObjects.begin();
+      it != ie.wholeObjects.end(); it ++){
+    thisSeen.insert(*it);
+  }
+  for(std::set<const Array *>::iterator it = thisSeen.begin(); it != thisSeen.end();
+      it ++){
+    returnVector.push_back(*it);
+  }
+}
+
 class IndependentSolver : public SolverImpl {
 private:
   Solver *solver;
@@ -285,10 +395,7 @@ public:
   bool computeInitialValues(const Query& query,
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution) {
-    return solver->impl->computeInitialValues(query, objects, values,
-                                              hasSolution);
-  }
+                            bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
   void setCoreSolverTimeout(double timeout);
@@ -321,6 +428,94 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
   return solver->impl->computeValue(Query(tmp, query.expr), result);
 }
 
+
+// Helper function used only for assertions to make sure point created
+// during computeInitialValues is in fact correct.
+bool assertCreatedPointEvaluatesToTrue(const Query &query,
+                                       const std::vector<const Array*> &objects,
+                                       std::vector< std::vector<unsigned char> > &values){
+  Assignment assign = Assignment(objects, values);
+  for(ConstraintManager::constraint_iterator it = query.constraints.begin();
+      it != query.constraints.end(); ++it){
+    ref<Expr> ret = assign.evaluate(*it);
+    if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){
+      return false;
+    }
+  }
+  ref<Expr> neg = Expr::createIsZero(query.expr);
+  ref<Expr> q = assign.evaluate(neg);
+
+  assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant");
+  return cast<ConstantExpr>(q)->isTrue();
+}
+
+bool IndependentSolver::computeInitialValues(const Query& query,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution){
+  std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>;
+  getAllIndependentConstraintsSets(query, factors);
+  //Used to rearrange all of the answers into the correct order
+  std::map<const Array*, std::vector<unsigned char> > retMap;
+  for (std::list<IndependentElementSet>::iterator it = factors->begin();
+       it != factors->end(); ++it) {
+    std::vector<const Array*> arraysInFactor;
+    calculateArrayReferences(*it, arraysInFactor);
+    // Going to use this as the "fresh" expression for the Query() invocation below
+    assert(it->exprs.size() >= 1 && "No null/empty factors");
+    if (arraysInFactor.size() == 0){
+      continue;
+    }
+    ConstraintManager tmp(it->exprs);
+    std::vector<std::vector<unsigned char> > tempValues;
+    if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)),
+                                            arraysInFactor, tempValues, hasSolution)){
+      values.clear();
+      return false;
+    } else if (!hasSolution){
+      values.clear();
+      return true;
+    } else {
+      assert(tempValues.size() == arraysInFactor.size() &&
+             "Should be equal number arrays and answers");
+      for (unsigned i = 0; i < tempValues.size(); i++){
+        if (retMap.count(arraysInFactor[i])){
+          // We already have an array with some partially correct answers,
+          // so we need to place the answers to the new query into the right
+          // spot while avoiding the undetermined values also in the array
+          std::vector<unsigned char> * tempPtr = &retMap[arraysInFactor[i]];
+          assert(tempPtr->size() == tempValues[i].size() &&
+                 "we're talking about the same array here");
+          ::DenseSet<unsigned> * ds = &(it->elements[arraysInFactor[i]]);
+          for (std::set<unsigned>::iterator it2 = ds->begin(); it2 != ds->end(); it2++){
+            unsigned index = * it2;
+            (* tempPtr)[index] = tempValues[i][index];
+          }
+        } else {
+          // Dump all the new values into the array
+          retMap[arraysInFactor[i]] = tempValues[i];
+        }
+      }
+    }
+  }
+  for (std::vector<const Array *>::const_iterator it = objects.begin();
+       it != objects.end(); it++){
+    const Array * arr = * it;
+    if (!retMap.count(arr)){
+      // this means we have an array that is somehow related to the
+      // constraint, but whose values aren't actually required to
+      // satisfy the query.
+      std::vector<unsigned char> ret(arr->size);
+      values.push_back(ret);
+    } else {
+      values.push_back(retMap[arr]);
+    }
+  }
+  assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation");
+  delete factors;
+  return true;
+}
+
 SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();      
 }
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index d976b0b4..8b69fd04 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
      reasonable. */
   klee_assume((s->st_blksize & ~0xFFFF) == 0);
 
-  klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
-  klee_prefer_cex(s, s->st_dev == defaults->st_dev);
-  klee_prefer_cex(s, s->st_rdev == defaults->st_rdev);
-  klee_prefer_cex(s, (s->st_mode&0700) == 0600);
-  klee_prefer_cex(s, (s->st_mode&0070) == 0020);
-  klee_prefer_cex(s, (s->st_mode&0007) == 0002);
-  klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
-  klee_prefer_cex(s, s->st_nlink == 1);
-  klee_prefer_cex(s, s->st_uid == defaults->st_uid);
-  klee_prefer_cex(s, s->st_gid == defaults->st_gid);
-  klee_prefer_cex(s, s->st_blksize == 4096);
-  klee_prefer_cex(s, s->st_atime == defaults->st_atime);
-  klee_prefer_cex(s, s->st_mtime == defaults->st_mtime);
-  klee_prefer_cex(s, s->st_ctime == defaults->st_ctime);
+  klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
+  klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev);
+  klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev);
+  klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600);
+  klee_posix_prefer_cex(s, (s->st_mode&0070) == 0020);
+  klee_posix_prefer_cex(s, (s->st_mode&0007) == 0002);
+  klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
+  klee_posix_prefer_cex(s, s->st_nlink == 1);
+  klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid);
+  klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid);
+  klee_posix_prefer_cex(s, s->st_blksize == 4096);
+  klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime);
+  klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime);
+  klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime);
 
   s->st_size = dfile->size;
   s->st_blocks = 8;
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 2a6b6f68..cbcf31f4 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -67,7 +67,7 @@ static char *__get_sym_str(int numChars, char *name) {
   klee_make_symbolic(s, numChars+1, name);
 
   for (i=0; i<numChars; i++)
-    klee_prefer_cex(s, __isprint(s[i]));
+    klee_posix_prefer_cex(s, __isprint(s[i]));
   
   s[numChars] = '\0';
   return s;
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index cf67e647..180e03cf 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --exit-on-error --prefer-cex %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
 // RUN: ktest-tool %t.klee-out/test000001.ktest | FileCheck %s
 
 #include <assert.h>
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 73e2783e..6b4fb8f4 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -418,6 +418,10 @@ void klee_prefer_cex(void *buffer, uintptr_t condition) {
   ;
 }
 
+void klee_posix_prefer_cex(void *buffer, uintptr_t condition) {
+  ;
+}
+
 void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
   /* XXX remove model version code once new tests gen'd */
   if (obj_index >= input->numObjects) {