From bd2ed196e3afde3d575affd127c42503dfde04c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Mar 2018 19:36:21 -0700 Subject: [PATCH] add correct badge Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- src/opt/opt_solver.cpp | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index e3ef58b70..8ebf6a078 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- | -[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +[![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index c5363816a..785836f56 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -229,6 +229,7 @@ namespace opt { inf_eps val = get_optimizer().maximize(v, blocker, has_shared); get_model(m_model); inf_eps val2; + std::cout << m_valid_objectives.size() << " " << i << "\n"; m_valid_objectives[i] = true; TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";); if (!m_models[i]) { @@ -341,6 +342,7 @@ namespace opt { smt::theory_var opt_solver::add_objective(app* term) { smt::theory_var v = get_optimizer().add_objective(term); + std::cout << "add objective " << v << "\n"; m_objective_vars.push_back(v); m_objective_values.push_back(inf_eps(rational(-1), inf_rational())); m_objective_terms.push_back(term); @@ -436,6 +438,7 @@ namespace opt { } void opt_solver::reset_objectives() { + std::cout << "reset-objectives\n"; m_objective_vars.reset(); m_objective_values.reset(); m_objective_terms.reset();