From 67cc2a8cf0d564416f3f24c789544ddbd2b9eade Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 Feb 2020 04:51:35 -0800
Subject: [PATCH] fix #2939

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b3bce3bb2..b677eb0f0 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1456,12 +1456,7 @@ br_status seq_rewriter::mk_str_lt(expr* a, expr* b, expr_ref& result) {
                 return BR_DONE;
             }
         }
-        if (sz <= as.length()) {
-            result = m().mk_false();
-        }
-        else {
-            result = m().mk_true();
-        }
+        result = m().mk_bool_val(as.length() < bs.length());
         return BR_DONE;
     }
     return BR_FAILED;