From 6f67e9cdda33df556b7026cb215a555b3db4170f Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 28 Jul 2016 17:18:56 -0400
Subject: [PATCH] fix theory_str::check_length_concat_concat to actually assert
 the conflict axiom

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 17246ccf8..6393d8154 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4261,6 +4261,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
 
     if (conflict) {
         TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;);
+        assert_axiom(toAssert);
         return false;
     }
     return true;