From f9d38a97df6465709b1215a633c2ab3ff0c97e1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 17:49:30 +0000 Subject: [PATCH] Bugfix for array simplifier Signed-off-by: Christoph M. Wintersteiger --- src/ast/simplifier/array_simplifier_plugin.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index 065f8bd96..b169babac 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -421,9 +421,6 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul tout << mk_pp(lhs, m_manager) << " = " << mk_pp(rhs, m_manager) << " := " << eq << "\n";); switch(eq) { - case l_false: - result = m_manager.mk_false(); - return true; case l_true: result = m_manager.mk_true(); return true;