mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
preparing for inf extension of arithmetic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0b65aa83e8
commit
5106c74b3e
5 changed files with 8 additions and 7 deletions
|
@ -43,7 +43,7 @@ Notes:
|
|||
#include "optimize_objectives.h"
|
||||
#include "opt_solver.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "smt_context.h"
|
||||
#include "theory_arith.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
|
@ -115,6 +115,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool optimize_objectives::update_upper() {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue