mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-27 06:29:38 -08:00
parent e969bd1c97
commit 0c770e25df
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/char_decl_plugin.cpp
View file

@ -110,6 +110,10 @@ expr* char_decl_plugin::get_some_value(sort* s) {
}
app* char_decl_plugin::mk_le(expr* a, expr* b) {
expr* es[2] = { a, b};
expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
unsigned v1 = 0, v2 = 0;
if (is_const_char(a, v1) && is_const_char(b, v2))
return m_manager->mk_bool_val(v1 <= v2);
expr* es[2] = { a, b };
return m_manager->mk_app(m_family_id, OP_CHAR_LE, 2, es);
}