diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index 52da9e823..e5a9bc482 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -23,13 +23,6 @@ namespace synth {
         
     solver::~solver() {}
 
-
-    // recognize synthesis objective as part of search objective.
-    // register it for calls to check.
-    void solver::asserted(sat::literal lit) {
-
-    }
-
     bool solver::synthesize(app* e) {
 
         if (e->get_num_args() == 0)
@@ -83,27 +76,6 @@ namespace synth {
         return sat::check_result::CR_DONE;
     }
 
-    // nothing particular to do
-    void solver::push_core() {
-
-    }
-
-    // nothing particular to do
-    void solver::pop_core(unsigned n) {
-    }
-
-    // nothing particular to do
-    bool solver::unit_propagate() {
-        return false;
-    }
-
-    // retrieve explanation for assertions made by synth solver. It only asserts unit literals so nothing to retrieve
-    void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) {
-    }
-
-    // where we collect statistics (number of invocations?)
-    void solver::collect_statistics(statistics& st) const {}
-
     // recognize synthesis objectives here.
     sat::literal solver::internalize(expr* e, bool sign, bool root) {
 	internalize(e);
@@ -126,22 +98,14 @@ namespace synth {
 
     // display current state (eg. current set of realizers)
     std::ostream& solver::display(std::ostream& out) const {
+        for (auto * e : m_synth)
+            out << "synth objective " << mk_pp(e, m) << "\n";            
         return out;
     }
 
-    // justified by "synth".
-    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
-        return out << "synth";
-    }
-    
-    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
-        return out << "synth";
-    }
-
     // create a clone of the solver.
     euf::th_solver* solver::clone(euf::solver& ctx) {
-        NOT_IMPLEMENTED_YET();
-        return nullptr;
+        return alloc(solver, ctx);
     }
 
 }
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index 56a640cce..ce302b579 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -21,26 +21,21 @@ Author:
 namespace synth {
 
     class solver : public euf::th_euf_solver {
-
     public:
         solver(euf::solver& ctx);
-        
-        ~solver() override;
-
-        
-        void asserted(sat::literal lit) override;
-
+        ~solver() override;        
+        void asserted(sat::literal lit) override {}
         sat::check_result check() override;
-        void push_core() override;
-        void pop_core(unsigned n) override;
-        bool unit_propagate() override;
-        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
-        void collect_statistics(statistics& st) const override;
+        void push_core() override {}
+        void pop_core(unsigned n) override {}
+        bool unit_propagate() override { return false; }
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override {}
+        void collect_statistics(statistics& st) const override {}
         sat::literal internalize(expr* e, bool sign, bool root) override;
         void internalize(expr* e) override;
         std::ostream& display(std::ostream& out) const override;
-        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
-        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out << "synth"; }
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out << "synth"; }
         euf::th_solver* clone(euf::solver& ctx) override;
 
     private: