mirror of
https://github.com/Z3Prover/z3
synced 2026-07-12 10:06:23 +00:00
guard update to depth bound to avoid overflow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a8e8498d9c
commit
a1b926fea3
1 changed files with 2 additions and 1 deletions
|
|
@ -2058,7 +2058,8 @@ namespace seq {
|
|||
return r;
|
||||
}
|
||||
// depth limit hit – double the bound and retry
|
||||
m_depth_bound *= 2;
|
||||
if (m_depth_bound < INT_MAX/2)
|
||||
m_depth_bound *= 2;
|
||||
SASSERT(m_depth_bound < INT_MAX);
|
||||
}
|
||||
++m_stats.m_num_unknown;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue