Minor fixes

src/reach/avr_config.cpp

@@ -26,7 +26,7 @@ int Config::g_forward_check = 0;
 int Config::g_fineness = 0;
 int Config::g_lazy_assume = 0;
 
-bool Config::g_uf_propagate = false;
+bool Config::g_uf_no_propagate = false;
 bool Config::g_uf_heavy_only = false;
 bool Config::g_uf_no_bitwise = false;
 bool Config::g_uf_no_sext = false;
@@ -247,8 +247,8 @@ void Config::set_abstraction(string& name) {
 	g_ab_interpret_excc = LEVEL_EXCC_DEFAULT;
 
 	{
-		if (name.find(NAME_UF_PROPAGATE) != string::npos)
-			g_uf_propagate = !g_uf_propagate;
+		if (name.find(NAME_UF_NO_PROPAGATE) != string::npos)
+			g_uf_no_propagate = !g_uf_no_propagate;
 		if (name.find(NAME_UF_HEAVY_ONLY) != string::npos)
 			g_uf_heavy_only = !g_uf_heavy_only;
 		if (name.find(NAME_UF_NO_BITWISE) != string::npos)
@@ -298,7 +298,7 @@ void Config::set_abstraction(string& name) {
 														 << (g_ab_interpret_limit == 0?"":to_string(g_ab_interpret_limit))
 														 << ((g_ab_interpret_excc != LEVEL_EXCC_DEFAULT)?"+ec"+to_string(g_ab_interpret_excc):"")
 														 << (g_fineness != FINENESS_DEFAULT?"+l"+to_string(g_fineness):"")
-														 << (g_uf_propagate?"+propagate":"")
+														 << (g_uf_no_propagate?"+nopropagate":"")
 														 << (g_uf_heavy_only?"+heavy":"")
 														 << (g_uf_no_bitwise?"+nobitwise":"")
 														 << (g_uf_no_sext?"+nosignex":"")

src/reach/avr_config.h

@@ -175,7 +175,7 @@
 #define NAME_SABV   "sa"
 #define NAME_EXCC   "ec"
 
-#define NAME_UF_PROPAGATE   "+propagate"
+#define NAME_UF_NO_PROPAGATE   "+nopropagate"
 #define NAME_UF_HEAVY_ONLY   "+heavy"
 #define NAME_UF_NO_BITWISE  "+nobitwise"
 #define NAME_UF_NO_SEXT     "+nosignex"
@@ -263,7 +263,7 @@ class Config {
 	static int g_forward_check;
 	static int g_fineness;
 	static int g_lazy_assume;
-	static bool g_uf_propagate;
+	static bool g_uf_no_propagate;
 	static bool g_uf_heavy_only;
 	static bool g_uf_no_bitwise;
 	static bool g_uf_no_sext;

src/reach/avr_word_netlist.cpp

@@ -3680,7 +3680,7 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify
 //					return e->t_simple;
 					// do nothing, done
 				}
-				else if (Config::g_uf_propagate) {
+				else if (!Config::g_uf_no_propagate) {
 					e->propagate_uf();
 				}
 			}

src/reach/reach_cegar.cpp

@@ -539,11 +539,13 @@ void Reach::refine(InstL& hardConstraints, ABSTRACT_CUBE& abCube, Inst *top_wo_r
 				else
 					hardConstraints.push_back(v.first);
 			}
-			for (auto& v: _assume_T) {
-				if (Config::g_lazy_assume > LAZY_ASSUME_NONE)
-					viol.push_back(v.first);
-				else
-					hardConstraints.push_back(v.first);
+			if (_frame_idx != 0) {
+				for (auto& v: _assume_T) {
+					if (Config::g_lazy_assume > LAZY_ASSUME_NONE)
+						viol.push_back(v.first);
+					else
+						hardConstraints.push_back(v.first);
+				}
 			}
 			if (!hardConstraints.empty()) {
 				viol.push_back(OpInst::create(OpInst::LogAnd, hardConstraints));
@@ -6120,14 +6122,13 @@ int Reach::verify() {
 						conjunct_prop.push_back(_ve_prop_eq_0);
 						conjunct_prop.push_back(_ve_model);
 						InstL conjunct_prop_wo_ref = conjunct_prop;
-						for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3)
+						for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3) {
+							if (*it3 == _ve_assume_T)
+								continue;
 							conjunct_prop.push_back(*it3);
+						}
 						if (Config::g_lazy_assume >= LAZY_ASSUME_L2)
 							conjunct_prop.push_back(_ve_assume);
-						if (Config::g_lazy_assume >= LAZY_ASSUME_L1) {
-							for (auto& v: _assume_T)
-								conjunct_prop.push_back(v.first);
-						}
 
 						ve_prop = OpInst::create(OpInst::LogAnd, conjunct_prop);
 						AVR_LOG(15, 0, "[Basis Step]:" << endl);

src/reach/reach_core.h

@@ -1554,6 +1554,7 @@ class Reach{
 	InstL _assume_wires;
 	InstS _assume_regNext;
 	InstToBoolM _assume_T;
+	Inst* _ve_assume_T;
 
 	InstL _assume_Twires;
 

src/reach/reach_util.cpp

@@ -7415,17 +7415,17 @@ void Reach::collect_system() {
 				assumeT.push_back(coneT);
 			}
 			if (!assumeT.empty()) {
-				Inst* tveAssume = OpInst::create(OpInst::LogAnd, assumeT);
-				add_all_wires(tveAssume, _assume_Twires, true);
+				_ve_assume_T = OpInst::create(OpInst::LogAnd, assumeT);
+				add_all_wires(_ve_assume_T, _assume_Twires, true);
 	  		if (Config::g_lazy_assume >= LAZY_ASSUME_L1) {
 					for (auto& v: assumeT) {
 							_assume_T.insert(make_pair(v, false));
 					}
 	  		}
 				else {
 					numAssumeLemmas++;
-					_negated_refs.push_back(tveAssume);
-					_assume_T.insert(make_pair(tveAssume, true));
+					_negated_refs.push_back(_ve_assume_T);
+					_assume_T.insert(make_pair(_ve_assume_T, true));
 				}
 			}
   	}