From: bdemsky <bdemsky@uci.edu>
Date: Wed, 10 May 2017 00:41:48 +0000 (-0700)
Subject: Need to allow for one spare encoding for the non-executed case with no suitable stores.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=34698794dfbc5f8f8e757f9ea4d9afa051157ec7;p=satcheck.git

Need to allow for one spare encoding for the non-executed case with no suitable stores.
---

diff --git a/loadrf.cc b/loadrf.cc
index 2d5984a..52a08fb 100644
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -18,7 +18,7 @@
 LoadRF::LoadRF(EPRecord *_load, ConstGen *cg) : load(_load) {
 	RecordSet *mrfSet=cg->getMayReadFromSet(load);
 	uint numstores=mrfSet->getSize();
-	numvars=NUMBITS(numstores-1);
+	numvars=NUMBITS(numstores); 
 	vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
 	cg->getArrayNewVars(numvars, vars);
 }
diff --git a/threads.cc b/threads.cc
index 52b7ca9..a3497e0 100644
--- a/threads.cc
+++ b/threads.cc
@@ -24,6 +24,10 @@
 /** Allocate a stack for a new thread. */
 static void * stack_allocate(size_t size)
 {
+	// TODO: This could be a bug if we have programs that start threads
+	// in different orders.  The solution is to use the same strategy
+	// the ALLOC action uses.
+
 	return snapshot_malloc(size);
 }