From e521ab2c3af04c7c4b4082a2ffc81b0c6caf864a Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 18 Oct 2015 19:39:55 -0400
Subject: [PATCH] fix concat_axiom loop in propagate(): compare against
 size()......

---
 src/smt/theory_str.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index aebaec572..47165997d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -376,7 +376,7 @@ void theory_str::propagate() {
         }
         m_str_eq_todo.reset();
 
-        for (unsigned i = 0; i < m_concat_axiom_todo.empty(); ++i) {
+        for (unsigned i = 0; i < m_concat_axiom_todo.size(); ++i) {
             instantiate_concat_axiom(m_concat_axiom_todo[i]);
         }
         m_concat_axiom_todo.reset();