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

fix #2122 for code that isn't exception safe

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-02 19:49:16 +01:00
parent a76107e50d
commit 9fde9fe3a2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/polynomial/upolynomial.cpp
View file

@ -524,11 +524,11 @@ namespace upolynomial {
set(sz1, p1, buffer); set(sz1, p1, buffer);
if (sz1 <= 1) if (sz1 <= 1)
return; return;
numeral const & b_n = p2[sz2-1]; numeral const & b_n = p2[sz2-1];
SASSERT(!m().is_zero(b_n)); SASSERT(!m().is_zero(b_n));
scoped_numeral a_m(m()); scoped_numeral a_m(m());
while (true) { while (m_limit.inc()) {
checkpoint();
TRACE("rem_bug", tout << "rem loop, p2:\n"; display(tout, sz2, p2); tout << "\nbuffer:\n"; display(tout, buffer); tout << "\n";); TRACE("rem_bug", tout << "rem loop, p2:\n"; display(tout, sz2, p2); tout << "\nbuffer:\n"; display(tout, buffer); tout << "\n";);
sz1 = buffer.size(); sz1 = buffer.size();
if (sz1 < sz2) { if (sz1 < sz2) {