diff --git a/src/ast/synth_decl_plugin.cpp b/src/ast/synth_decl_plugin.cpp
index f6c4a88f0..221b7a0ca 100644
--- a/src/ast/synth_decl_plugin.cpp
+++ b/src/ast/synth_decl_plugin.cpp
@@ -43,6 +43,9 @@ namespace synth {
         case OP_DECLARE_GRAMMAR: 
 	    name = "uncomputable";
 	    break;
+        case OP_DECLARE_SPECIFICATION: 
+	    name = "constraint";
+	    break;
         default:
             NOT_IMPLEMENTED_YET();
         }
@@ -54,6 +57,7 @@ namespace synth {
         if (logic == symbol::null) {
             op_names.push_back(builtin_name("synthesiz3", OP_DECLARE_OUTPUT));
             op_names.push_back(builtin_name("uncomputable", OP_DECLARE_GRAMMAR));
+            op_names.push_back(builtin_name("constraint", OP_DECLARE_SPECIFICATION));
         }
     }
 
diff --git a/src/ast/synth_decl_plugin.h b/src/ast/synth_decl_plugin.h
index 01d606764..c3b502d22 100644
--- a/src/ast/synth_decl_plugin.h
+++ b/src/ast/synth_decl_plugin.h
@@ -24,6 +24,7 @@ namespace synth {
     enum op_kind {
         OP_DECLARE_OUTPUT,
         OP_DECLARE_GRAMMAR,
+	OP_DECLARE_SPECIFICATION,
         LAST_OP
     };
     
@@ -51,6 +52,7 @@ namespace synth {
         
         bool is_synthesiz3(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); }
         bool is_grammar(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); }
+        bool is_specification(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_SPECIFICATION); }
     };
     
 }
diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index 0292c3d46..dcc7a35b6 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -85,6 +85,16 @@ namespace synth {
         }
     }
 
+    void solver::add_specification(app* e) {
+	// This assumes that each (assert (constraint (...)) is asserting exactly one app
+	SASSERT((e->get_num_args() == 1) && (is_app(e->get_arg(0))));
+	app* arg = to_app(e->get_arg(0));
+	internalize(arg);
+	m_spec.insert(arg);
+	ctx.push(insert_obj_trail(m_spec, arg));
+	// TODO: assert arg <=> e
+    }
+
     // recognize synthesis objectives here.
     sat::literal solver::internalize(expr* e, bool sign, bool root) {
         internalize(e);
@@ -101,10 +111,13 @@ namespace synth {
         sat::literal lit(bv, false);
 	ctx.attach_lit(lit, e);
         synth::util util(m);
+	app* a = to_app(e);
         if (util.is_synthesiz3(e))
-            add_synth_objective(to_app(e));
+            add_synth_objective(a);
         if (util.is_grammar(e))
-	    add_uncomputable(to_app(e));
+	    add_uncomputable(a);
+	if (util.is_specification(e))
+	    add_specification(a);
     }
 
     // display current state (eg. current set of realizers)
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index f28d37e77..79404d8b4 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -42,6 +42,7 @@ namespace synth {
         sat::literal synthesize(app* e);
 	void add_uncomputable(app* e);
         void add_synth_objective(app* e);
+	void add_specification(app* e);
 	bool contains_uncomputable(expr* e);
 
         void on_merge_eh(euf::enode* root, euf::enode* other);
@@ -54,6 +55,8 @@ namespace synth {
     	ptr_vector<app> m_synth;
         typedef obj_hashtable<func_decl> func_decl_set;
 	func_decl_set m_uncomputable;
+	typedef obj_hashtable<app> app_set;
+	app_set m_spec;
 
     };