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

add e_internalized() check in theory_str::get_arith_value()

Browse source
This commit is contained in:
Murphy Berzish 2017-07-19 10:15:38 -04:00
parent 69f0ed9b1f
commit 7ddb940f77
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -4656,6 +4656,11 @@ namespace smt {
context& ctx = get_context();
ast_manager & m = get_manager();
// safety
if (!ctx.e_internalized(e)) {
return false;
}
// if an integer constant exists in the eqc, it should be the root
enode * en_e = ctx.get_enode(e);
enode * root_e = en_e->get_root();