X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=loadrf.cc;h=f536c1bf336d2340012f4dd3231d99dc58d18e47;hb=0174ae3f85cabaca148065bb9a83019dc5260e64;hp=1b9c551b01d3887dda68605651465dbbf86405f5;hpb=2d4cabdb7443e9961771abd265d7c8f434c01033;p=satcheck.git

diff --git a/loadrf.cc b/loadrf.cc
index 1b9c551..f536c1b 100644
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -84,12 +84,28 @@ void LoadRF::genConstraints(ConstGen *cg) {
 			Constraint * storebeforeconflict=cg->getOrderConstraint(store, conflictstore);
 			if (storebeforeconflict->isFalse())
 				continue;
+#ifdef TSO
+			//Have to cover the same thread case
+			Constraint *conflictbeforeload;
+			if (conflictstore->getEP()->get_tid()==load->getEP()->get_tid()) {
+				if (conflictstore->getEP()->compare(load->getEP())==CR_AFTER)
+					conflictbeforeload=&ctrue;
+				else
+					conflictbeforeload=&cfalse;
+			} else {
+				conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
+			}
+			if (conflictbeforeload->isFalse()) {
+				storebeforeconflict->freerec();
+				continue;
+			}
+#else
 			Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);	
 			if (conflictbeforeload->isFalse()) {
 				storebeforeconflict->freerec();
 				continue;
 			}
-
+#endif
 			rfconst=generateConstraint(numvars, vars, storeindex);
 			Constraint *array[]={storebeforeconflict,
 													 conflictbeforeload,