From f375016a11cd97d64de8ed35bd15def6aec4a162 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Jun 2017 18:23:27 -0500
Subject: [PATCH] disable tweak to seq until there are cycles to test further
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_seq.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3b70e1426..4dfff21c2 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2180,7 +2180,7 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
}
bool theory_seq::internalize_atom(app* a, bool) {
-#if 0
+#if 1
return internalize_term(a);
#else
if (is_skolem(m_eq, a)) {