diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index 62ebcf5e4..20de66fb3 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -92,8 +92,7 @@ namespace synth {
         sat::literal lit_e(bv, false);
 	ctx.attach_lit(lit_e, e);
         add_clause(~lit_e, lit);
-	m_spec.insert(arg);
-	ctx.push(insert_obj_trail(m_spec, arg));
+	ctx.push_vec(m_spec, arg);        
     }
 
     // recognize synthesis objectives here.
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index cd54a510f..6c72b599d 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -56,10 +56,8 @@ namespace synth {
         ptr_vector<app> m_solved;
 
     	ptr_vector<app> m_synth;
-        typedef obj_hashtable<func_decl> func_decl_set;
-	func_decl_set m_uncomputable;
-	typedef obj_hashtable<app> app_set;
-        obj_hashtable<expr> m_spec;
+	obj_hashtable<func_decl> m_uncomputable;
+        ptr_vector<expr> m_spec;
 
     };