mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix #1316, segmentation fault when numeric value is not internalized

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-21 18:56:36 -04:00
parent b2191cab02
commit 42fbe19814
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/smt/theory_seq.cpp
View file

@ -3466,6 +3466,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v)
bool theory_seq::get_num_value(expr* e, rational& val) const {
context& ctx = get_context();
expr_ref _val(m);
if (!ctx.e_internalized(e))
return false;
enode* next = ctx.get_enode(e), *n = next;
do {
if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {