From 0be3d016f644ba4cd42c400644b4ef77ffcf4b30 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 9 Aug 2023 18:35:05 -0700
Subject: [PATCH] updates with constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/synth_solver.cpp | 3 +--
 src/sat/smt/synth_solver.h   | 6 ++----
 2 files changed, 3 insertions(+), 6 deletions(-)

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;
 
     };