mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

equality simplification

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-31 15:44:43 -08:00
parent 6d99a8f0cc
commit 942706e271
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/char_decl_plugin.cpp
View file

@ -114,6 +114,8 @@ expr* char_decl_plugin::get_some_value(sort* s) {
app* char_decl_plugin::mk_le(expr* a, expr* b) {
expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
unsigned v1 = 0, v2 = 0;
if (a == b)
return m_manager->mk_true();
bool c1 = is_const_char(a, v1);
bool c2 = is_const_char(b, v2);
if (c1 && c2)