mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fixed bugs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
189fc46b6d
commit
47edff2076
|
@ -150,6 +150,7 @@ extern "C" {
|
|||
r = au(c).mk_numeral(_r, false); \
|
||||
} \
|
||||
} \
|
||||
mk_c(c)->save_ast_trail(r); \
|
||||
RETURN_Z3(of_ast(r));
|
||||
|
||||
|
||||
|
@ -222,6 +223,7 @@ extern "C" {
|
|||
_am.root(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -243,6 +245,7 @@ extern "C" {
|
|||
_am.power(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
|
|
@ -260,8 +260,8 @@ public:
|
|||
\brief c <- a - b
|
||||
*/
|
||||
void sub(interval const & a, interval const & b, interval & c) {
|
||||
m().sub(a.m_lower, b.m_lower, c.m_lower);
|
||||
m().sub(a.m_upper, b.m_upper, c.m_upper);
|
||||
m().sub(a.m_lower, b.m_upper, c.m_lower);
|
||||
m().sub(a.m_upper, b.m_lower, c.m_upper);
|
||||
}
|
||||
|
||||
private:
|
||||
|
|
Loading…
Reference in a new issue