mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Revert "Bugfix for array simplifier"

Browse source 
This reverts commit f9d38a97df.
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 17:53:06 +00:00
parent f9d38a97df
commit 0298519b4f
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -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;