From 0298519b4fe518da49c61c2a63be850a9fde7702 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 17:53:06 +0000 Subject: [PATCH] Revert "Bugfix for array simplifier" This reverts commit f9d38a97df6465709b1215a633c2ab3ff0c97e1a. --- src/ast/simplifier/array_simplifier_plugin.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index b169babac..065f8bd96 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -421,6 +421,9 @@ 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;