mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Bugfix for array simplifier

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 17:49:30 +00:00
parent d7a37f246c
commit f9d38a97df
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -421,9 +421,6 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
tout << mk_pp(lhs, m_manager) << " = " tout << mk_pp(lhs, m_manager) << " = "
<< mk_pp(rhs, m_manager) << " := " << eq << "\n";); << mk_pp(rhs, m_manager) << " := " << eq << "\n";);
switch(eq) { switch(eq) {
case l_false:
result = m_manager.mk_false();
return true;
case l_true: case l_true:
result = m_manager.mk_true(); result = m_manager.mk_true();
return true; return true;