mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

with const

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-14 21:57:53 -07:00
parent b21845cf72
commit 2481e6b910
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/synth_solver.cpp
View file

@ -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) {

2
src/sat/smt/synth_solver.h
View file

@ -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);