mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
minor fixes after feedback from regression tests...
This commit is contained in:
parent
b629dd7fdd
commit
cb8a6db51b
|
@ -1452,7 +1452,10 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
}
|
||||
}
|
||||
std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size());
|
||||
result = m_util.mk_concat(exs.size(), exs.c_ptr());
|
||||
if (exs.size() == 1)
|
||||
result = exs[0];
|
||||
else
|
||||
result = m_util.mk_concat(exs.size(), exs.c_ptr());
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
|
|
@ -1893,6 +1893,8 @@ namespace smt2 {
|
|||
if (!curr_is_rparen()) {
|
||||
check_int("invalid push command, integer expected");
|
||||
rational n = curr_numeral();
|
||||
if (n.is_neg())
|
||||
throw parser_exception("invalid push command, value is negative.");
|
||||
if (!n.is_unsigned())
|
||||
throw parser_exception("invalid push command, value is too big to fit in an unsigned machine integer");
|
||||
num = n.get_unsigned();
|
||||
|
|
Loading…
Reference in a new issue