From 5c47f244e9194f6caeefaf4cd3662b1d312cb288 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Feb 2021 03:37:14 -0800
Subject: [PATCH] fix #5047

---
 src/smt/theory_seq.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 244057521..c93666282 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -496,8 +496,10 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
     }
     TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
     literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
+    if (ctx.get_assignment(a) == l_false)
+        return false;
     literal b = mk_seq_eq(seq, e);
-    if (ctx.get_assignment(a) == l_false || ctx.get_assignment(b) == l_true)
+    if (ctx.get_assignment(b) == l_true)
         return false;
     add_axiom(~a, b);
     if (!ctx.at_base_level()) {