From 2481e6b91035ad7992f9f07d96d1378ddc5daa4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Aug 2023 21:57:53 -0700 Subject: [PATCH] with const Signed-off-by: Nikolaj Bjorner --- src/sat/smt/synth_solver.cpp | 2 +- src/sat/smt/synth_solver.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index e0cef522c..8b49fc1a2 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -51,7 +51,7 @@ namespace synth { } } - void solver::add_synth_objective(synth_objective& e) { + void solver::add_synth_objective(synth_objective const& e) { m_synth.push_back(e); ctx.push(push_back_vector(m_synth)); for (auto* arg : e) { diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h index 53a834b84..4803b3f16 100644 --- a/src/sat/smt/synth_solver.h +++ b/src/sat/smt/synth_solver.h @@ -65,7 +65,7 @@ namespace synth { sat::literal synthesize(synth_objective const& synth_objective); void add_uncomputable(app* e); - void add_synth_objective(synth_objective & e); + void add_synth_objective(synth_objective const & e); void add_specification(app* e, expr* arg); bool contains_uncomputable(expr* e); void on_merge_eh(euf::enode* root, euf::enode* other);