From 73ab95d3383058a2b1a2120e615d3a410e176f7e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Mar 2020 12:47:30 -0700
Subject: [PATCH] remove canonize in seq solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 0537dd765..a46ffaa92 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3485,9 +3485,11 @@ bool theory_seq::solve_nc(unsigned idx) {
     lbool is_gt = ctx.get_assignment(len_gt);
     TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
 
+#if 0
     if (canonizes(false, n.contains())) {
         return true;
     }
+#endif
     
     switch (is_gt) {
     case l_true: