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;