From a76107e50d3a75dc4404d72af6d25e6e42d576cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Feb 2019 18:44:52 -0800 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 1 - src/muz/spacer/spacer_iuc_solver.h | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 725ac33b4..4de05d31c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7344,7 +7344,6 @@ class Optimize(Z3PPObject): >>> x = Int('x') >>> p3 = Bool('p3') >>> s = Optimize() - >>> s.set(unsat_core=True) >>> s.assert_and_track(x > 0, 'p1') >>> s.assert_and_track(x != 1, 'p2') >>> s.assert_and_track(x < 0, p3) diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index 67fdc0fc3..c3561a6d4 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -123,7 +123,7 @@ public: void assert_expr_core2(expr *t, expr *a) override { NOT_IMPLEMENTED_YET(); } expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } void get_levels(ptr_vector const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); } - expr_ref_vector get_trail() { return m_solver.get_trail(); } + expr_ref_vector get_trail() override { return m_solver.get_trail(); } void push() override; void pop(unsigned n) override;