From dcb81f0ad26c5878a4e53275653072b62cd10ffb Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 22 Feb 2020 20:44:20 -0800
Subject: [PATCH] introduce a bug int theory_array.cpp - look for a counter
 example

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_array.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index eb4f87e63..703423f8f 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -296,7 +296,7 @@ namespace smt {
     }
 
     void theory_array::apply_sort_cnstr(enode * n, sort * s) {
-        //        return;
+        return;
         SASSERT(is_array_sort(s));
         if (!is_attached_to_var(n))
             mk_var(n);