From 5dbe4a6c8b77cd5be1a68a564602550317cc4f41 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 22 Feb 2020 14:17:31 -0800
Subject: [PATCH] introduce a bug into theory_array - looking for a
 counterexample

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

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