mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
adjust for SMTLIBification name change of set operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c9b906a518
commit
9f1b8db870
|
@ -4582,7 +4582,7 @@ def SetIntersect(*args):
|
|||
>>> a = Const('a', SetSort(IntSort()))
|
||||
>>> b = Const('b', SetSort(IntSort()))
|
||||
>>> SetIntersect(a, b)
|
||||
intersect(a, b)
|
||||
intersection(a, b)
|
||||
"""
|
||||
args = _get_args(args)
|
||||
ctx = _ctx_from_ast_arg_list(args)
|
||||
|
@ -4623,7 +4623,7 @@ def SetDifference(a, b):
|
|||
>>> a = Const('a', SetSort(IntSort()))
|
||||
>>> b = Const('b', SetSort(IntSort()))
|
||||
>>> SetDifference(a, b)
|
||||
difference(a, b)
|
||||
setminus(a, b)
|
||||
"""
|
||||
ctx = _ctx_from_ast_arg_list([a, b])
|
||||
return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
|
||||
|
|
|
@ -1116,7 +1116,9 @@ namespace opt {
|
|||
val = (*mdl)(term);
|
||||
unsigned bvsz;
|
||||
if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
|
||||
TRACE("opt", tout << "model does not evaluate objective to a value\n";);
|
||||
TRACE("opt", tout << "model does not evaluate objective to a value but instead " << val << "\n";
|
||||
tout << *mdl << "\n";
|
||||
);
|
||||
return false;
|
||||
}
|
||||
if (r != v) {
|
||||
|
|
Loading…
Reference in a new issue