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

fix for null symbol #2712

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-18 12:55:16 -08:00
parent 37382d22c4
commit 05ad90c976
2 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/c++/z3++.h
View file

@ -1674,6 +1674,20 @@ namespace z3 {
return func_decl(c, f);
}
/**
\brief signed less than or equal to operator for bitvectors.
*/
inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed less than operator for bitvectors.
*/
inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief unsigned less than or equal to operator for bitvectors.
*/
@ -2337,7 +2351,7 @@ namespace z3 {
check_error();
return to_check_result(r);
}
check_result check(expr_vector assumptions) {
check_result check(expr_vector const& assumptions) {
unsigned n = assumptions.size();
array<Z3_ast> _assumptions(n);
for (unsigned i = 0; i < n; i++) {

4
src/util/symbol.cpp
View file

@ -141,6 +141,10 @@ bool lt(symbol const & s1, symbol const & s2) {
SASSERT(!s1.is_numerical());
return false;
}
if (!s1.bare_str())
return true;
if (!s2.bare_str())
return false;
SASSERT(!s1.is_numerical() && !s2.is_numerical());
auto cmp = strcmp(s1.bare_str(), s2.bare_str());
SASSERT(cmp != 0);