diff --git a/src/ast/jobshop_decl_plugin.cpp b/src/ast/jobshop_decl_plugin.cpp
index 7a7b1b590..b1abc7fa3 100644
--- a/src/ast/jobshop_decl_plugin.cpp
+++ b/src/ast/jobshop_decl_plugin.cpp
@@ -23,14 +23,17 @@ Revision History:
 void jobshop_decl_plugin::set_manager(ast_manager* m, family_id fid) {
     decl_plugin::set_manager(m, fid);
     m_int_sort = m_manager->mk_sort(m_manager->mk_family_id("arith"), INT_SORT);
+    m_alist_sort = m_manager->mk_sort(symbol("AList"), sort_info(m_family_id, ALIST_SORT));
     m_job_sort = m_manager->mk_sort(symbol("Job"), sort_info(m_family_id, JOB_SORT));
     m_resource_sort = m_manager->mk_sort(symbol("Resource"), sort_info(m_family_id, RESOURCE_SORT));
     m_manager->inc_ref(m_int_sort);
     m_manager->inc_ref(m_resource_sort);
     m_manager->inc_ref(m_job_sort);
+    m_manager->inc_ref(m_alist_sort);
 }
 
 void jobshop_decl_plugin::finalize() {
+    m_manager->dec_ref(m_alist_sort);
     m_manager->dec_ref(m_job_sort);
     m_manager->dec_ref(m_resource_sort);
     m_manager->dec_ref(m_int_sort);
@@ -43,12 +46,13 @@ sort * jobshop_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parame
     switch (static_cast<js_sort_kind>(k)) {
     case JOB_SORT: return m_job_sort;
     case RESOURCE_SORT: return m_resource_sort;
+    case ALIST_SORT: return m_alist_sort;
     default: UNREACHABLE(); return nullptr;
     }    
 }
 
 func_decl * jobshop_decl_plugin::mk_func_decl(
-    decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const *, sort *) {
+    decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) {
     switch (static_cast<js_op_kind>(k)) {
     case OP_JS_JOB:       
         check_arity(arity);
@@ -70,6 +74,18 @@ func_decl * jobshop_decl_plugin::mk_func_decl(
         check_arity(arity);
         check_index1(num_parameters, parameters);
         return m_manager->mk_func_decl(symbol("job2resource"), 0, (sort* const*)nullptr, m_int_sort, func_decl_info(m_family_id, k, num_parameters, parameters));
+    case OP_JS_MODEL:
+        // has no parameters
+        // all arguments are of sort alist
+        return m_manager->mk_func_decl(symbol("js-model"), arity, domain, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters));
+    case OP_AL_KV:
+        // has two parameters, first is symbol
+        // has no arguments
+        return m_manager->mk_func_decl(symbol("kv"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters));                
+    case OP_AL_LIST:
+        // has no parameters
+        // all arguments are of sort alist        
+        return m_manager->mk_func_decl(symbol("alist"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters));        
     default: 
         UNREACHABLE(); return nullptr;        
     }    
@@ -96,17 +112,20 @@ bool jobshop_decl_plugin::is_value(app * e) const {
 }
 
 void jobshop_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
-    if (logic == symbol("JOBSHOP")) {
+    if (logic == symbol("CSP")) {
         op_names.push_back(builtin_name("job", OP_JS_JOB));
         op_names.push_back(builtin_name("resource", OP_JS_RESOURCE));
         op_names.push_back(builtin_name("job-start", OP_JS_START));
         op_names.push_back(builtin_name("job-end", OP_JS_END));
         op_names.push_back(builtin_name("job2resource", OP_JS_JOB2RESOURCE));
+        op_names.push_back(builtin_name("js-model", OP_JS_MODEL));
+        op_names.push_back(builtin_name("kv", OP_AL_KV));
+        op_names.push_back(builtin_name("alist", OP_AL_LIST));
     }
 }
 
 void jobshop_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
-    if (logic == symbol("JOBSHOP")) {
+    if (logic == symbol("CSP")) {
         sort_names.push_back(builtin_name("Job", JOB_SORT));
         sort_names.push_back(builtin_name("Resource", RESOURCE_SORT));
     }
@@ -124,7 +143,7 @@ expr * jobshop_decl_plugin::get_some_value(sort * s) {
 
 
 jobshop_util::jobshop_util(ast_manager& m): m(m) {
-    m_fid = m.mk_family_id("jobshop");
+    m_fid = m.mk_family_id("csp");
     m_plugin = static_cast<jobshop_decl_plugin*>(m.get_plugin(m_fid));
 }
 
@@ -174,3 +193,11 @@ app* jobshop_util::mk_job2resource(unsigned j) {
     return m.mk_const(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 1, &p, 0, (sort*const*)nullptr, nullptr));
 }
 
+bool jobshop_util::is_resource(expr* e, unsigned& r) {
+    return is_app_of(e, m_fid, OP_JS_RESOURCE) && (r = resource2id(e), true);
+}
+
+bool jobshop_util::is_job(expr* e, unsigned& j) {
+    return is_app_of(e, m_fid, OP_JS_JOB) && (j = job2id(e), true);
+}
+
diff --git a/src/ast/jobshop_decl_plugin.h b/src/ast/jobshop_decl_plugin.h
index 48bdde6c1..f2cc7a849 100644
--- a/src/ast/jobshop_decl_plugin.h
+++ b/src/ast/jobshop_decl_plugin.h
@@ -68,7 +68,8 @@ Revision History:
 
 enum js_sort_kind {
     JOB_SORT,
-    RESOURCE_SORT
+    RESOURCE_SORT,
+    ALIST_SORT
 };
 
 enum js_op_kind {
@@ -76,7 +77,10 @@ enum js_op_kind {
     OP_JS_RESOURCE,          // value of type resource
     OP_JS_START,             // start time of a job
     OP_JS_END,               // end time of a job
-    OP_JS_JOB2RESOURCE       // resource associated with job
+    OP_JS_JOB2RESOURCE,      // resource associated with job
+    OP_JS_MODEL,             // jobscheduler model
+    OP_AL_KV,                // key-value pair
+    OP_AL_LIST               // tagged list
 };
 
 class jobshop_decl_plugin : public decl_plugin {
@@ -96,9 +100,11 @@ public:
     expr * get_some_value(sort * s) override;
     sort * mk_job_sort() const { return m_job_sort; }
     sort * mk_resource_sort() const { return m_resource_sort; }
+    sort * mk_alist_sort() const { return m_alist_sort; }
 private:
     sort* m_job_sort;
     sort* m_resource_sort;
+    sort* m_alist_sort;
     sort* m_int_sort;
 
     void check_arity(unsigned arity);
@@ -116,12 +122,59 @@ public:
     sort* mk_resource_sort();
 
     app* mk_job(unsigned j);
+    bool is_job(expr* e, unsigned& j);
     unsigned job2id(expr* j);
 
     app* mk_resource(unsigned r);
+    bool is_resource(expr* e, unsigned& r);
     unsigned resource2id(expr* r);
 
     app* mk_start(unsigned j);
     app* mk_end(unsigned j);
     app* mk_job2resource(unsigned j);
+
+    // alist features
+    app* mk_kv(symbol const& key, rational const& r) { 
+        parameter ps[2] = { parameter(key), parameter(r) };
+        return m.mk_const(m.mk_func_decl(m_fid, OP_AL_KV, 2, ps, 0, (sort*const*)nullptr, nullptr)); 
+    }
+    app* mk_kv(symbol const& key, symbol const& val) {
+        parameter ps[2] = { parameter(key), parameter(val) };
+        return m.mk_const(m.mk_func_decl(m_fid, OP_AL_KV, 2, ps, 0, (sort*const*)nullptr, nullptr)); 
+    }
+    app* mk_alist(symbol const& key, unsigned n, expr* const* args) {
+        parameter p(key);
+        return m.mk_app(m.mk_func_decl(m_fid, OP_AL_LIST, 1, &p, n, args, nullptr), n, args);
+
+    }
+    bool is_kv(expr* e, symbol& key, rational& r) {
+        return 
+            (is_app_of(e, m_fid, OP_AL_KV) && 
+             to_app(e)->get_decl()->get_num_parameters() == 2 &&
+             to_app(e)->get_decl()->get_parameter(1).is_rational() && 
+             (r = to_app(e)->get_decl()->get_parameter(1).get_rational(), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true)) ||
+            (is_app_of(e, m_fid, OP_AL_KV) && 
+             to_app(e)->get_decl()->get_num_parameters() == 2 &&
+             to_app(e)->get_decl()->get_parameter(1).is_int() && 
+             (r = rational(to_app(e)->get_decl()->get_parameter(1).get_int()), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true));
+
+
+    }
+    bool is_kv(expr* e, symbol& key, symbol& s) {
+        return is_app_of(e, m_fid, OP_AL_KV) && 
+            to_app(e)->get_decl()->get_num_parameters() == 2 &&
+            to_app(e)->get_decl()->get_parameter(1).is_symbol() && 
+            (s = to_app(e)->get_decl()->get_parameter(1).get_symbol(), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true);
+    }
+
+    bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); }
+    bool is_alist(expr* e) const { return is_app_of(e, m_fid, OP_AL_LIST); }
+    bool is_alist(expr* e, symbol& key) const { 
+        return is_alist(e) && 
+            to_app(e)->get_decl()->get_num_parameters() == 1 && 
+            to_app(e)->get_decl()->get_parameter(0).is_symbol() && 
+            (key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true); 
+    }
+
+    // app* mk_model(unsigned n, expr* const* alist);
 };
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index be3acc261..8387722b9 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -30,6 +30,7 @@ Notes:
 #include "ast/seq_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
+#include "ast/jobshop_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/pp.h"
@@ -695,6 +696,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
+        register_plugin(symbol("csp"),      alloc(jobshop_decl_plugin), smt_logics::logic_is_csp(m_logic));
     }
     else {
         // the manager was created by an external module
@@ -709,6 +711,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
+        load_plugin(symbol("csp"),      smt_logics::logic_is_csp(m_logic), fids);
         for (family_id fid : fids) {
             decl_plugin * p = m_manager->get_plugin(fid);
             if (p) {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 403ea4c85..d1b4847cc 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1523,8 +1523,20 @@ namespace smt2 {
             unsigned num_indices = 0;
             while (!curr_is_rparen()) {
                 if (curr_is_int()) {
-                    unsigned u = curr_unsigned();
-                    m_param_stack.push_back(parameter(u));
+                    if (!curr_numeral().is_unsigned()) {
+                        m_param_stack.push_back(parameter(curr_numeral()));                       
+                    }
+                    else {
+                        m_param_stack.push_back(parameter(curr_unsigned()));
+                    }
+                    next();
+                }
+                else if (curr_is_float()) {
+                    m_param_stack.push_back(parameter(curr_numeral()));
+                    next();
+                }
+                else if (curr_is_keyword()) {
+                    m_param_stack.push_back(parameter(curr_id()));
                     next();
                 }
                 else if (curr_is_identifier() || curr_is_lparen()) {
diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp
index ecf924111..ce4c0d9a9 100644
--- a/src/smt/smt_arith_value.cpp
+++ b/src/smt/smt_arith_value.cpp
@@ -30,7 +30,6 @@ namespace smt {
 
     bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) {
         if (!m_ctx.e_internalized(e)) return false;
-        expr_ref _lo(m);
         family_id afid = a.get_family_id();
         is_strict = false;
         enode* next = m_ctx.get_enode(e), *n = next;
@@ -42,15 +41,9 @@ namespace smt {
         theory_i_arith*  thi = dynamic_cast<theory_i_arith*>(th);
         theory_lra*      thr = dynamic_cast<theory_lra*>(th);
         do {
-            if (tha && tha->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
-                if (!found || lo1 > lo) lo = lo1;
-                found = true;
-            }
-            else if (thi && thi->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
-                if (!found || lo1 > lo) lo = lo1;
-                found = true;
-            }
-            else if (thr && thr->get_lower(next, lo1, is_strict1)) {
+            if ((tha && tha->get_lower(next, lo1, is_strict1)) ||
+                (thi && thi->get_lower(next, lo1, is_strict1)) ||
+                (thr && thr->get_lower(next, lo1, is_strict1))) {
                 if (!found || lo1 > lo || (lo == lo1 && is_strict1)) lo = lo1, is_strict = is_strict1;
                 found = true;
             }
@@ -62,7 +55,6 @@ namespace smt {
 
     bool arith_value::get_up(expr* e, rational& up, bool& is_strict) {
         if (!m_ctx.e_internalized(e)) return false;
-        expr_ref _up(m);
         family_id afid = a.get_family_id();
         is_strict = false;
         enode* next = m_ctx.get_enode(e), *n = next;
@@ -73,15 +65,9 @@ namespace smt {
         theory_i_arith*  thi = dynamic_cast<theory_i_arith*>(th);
         theory_lra*      thr = dynamic_cast<theory_lra*>(th);
         do {
-            if (tha && tha->get_upper(next, _up) && a.is_numeral(_up, up1)) {
-                if (!found || up1 < up) up = up1;
-                found = true;
-            }
-            else if (thi && thi->get_upper(next, _up) && a.is_numeral(_up, up1)) {
-                if (!found || up1 < up) up = up1;
-                found = true;
-            }
-            else if (thr && thr->get_upper(next, up1, is_strict1)) {
+            if ((tha && tha->get_upper(next, up1, is_strict1)) ||
+                (thi && thi->get_upper(next, up1, is_strict1)) ||
+                (thr && thr->get_upper(next, up1, is_strict1))) {
                 if (!found || up1 < up || (up1 == up && is_strict1)) up = up1, is_strict = is_strict1;
                 found = true;
             }
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 4b3ee52f6..a2c6c1191 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1071,6 +1071,8 @@ namespace smt {
 
         bool get_lower(enode* n, expr_ref& r);
         bool get_upper(enode* n, expr_ref& r);
+        bool get_lower(enode* n, rational& r, bool &is_strict);
+        bool get_upper(enode* n, rational& r, bool &is_strict);
         bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);
 
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 54f61a09a..1eb91f1fc 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3303,6 +3303,20 @@ namespace smt {
         return b && to_expr(b->get_value(), is_int(v), r);
     }
 
+    template<typename Ext>
+    bool theory_arith<Ext>::get_lower(enode * n, rational& r, bool& is_strict) {
+        theory_var v = n->get_th_var(get_id());
+        bound* b = (v == null_theory_var) ? nullptr : lower(v);
+        return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_pos(), true);
+    }
+
+    template<typename Ext>
+     bool theory_arith<Ext>::get_upper(enode * n, rational& r, bool& is_strict) {
+        theory_var v = n->get_th_var(get_id());
+        bound* b = (v == null_theory_var) ? nullptr : upper(v);
+        return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_neg(), true);
+    }
+
     // -----------------------------------
     //
     // Backtracking
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 173d44c52..5064fc037 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -65,7 +65,7 @@ namespace smt {
             unsigned j = u.job2id(term);
             app_ref start(u.mk_start(j), m);
             app_ref end(u.mk_end(j), m);
-            app_ref res(u.mk_resource(j), m);
+            app_ref res(u.mk_job2resource(j), m);
             if (!ctx.e_internalized(start)) ctx.internalize(start, false);
             if (!ctx.e_internalized(end))   ctx.internalize(end, false);
             if (!ctx.e_internalized(res))   ctx.internalize(res, false);
@@ -75,7 +75,7 @@ namespace smt {
             m_jobs.reserve(j + 1);
             m_jobs[j].m_start    = ctx.get_enode(start);
             m_jobs[j].m_end      = ctx.get_enode(end);
-            m_jobs[j].m_resource = ctx.get_enode(res);
+            m_jobs[j].m_job2resource = ctx.get_enode(res);
             ctx.attach_th_var(e, this, v);
             break;
         }
@@ -99,6 +99,89 @@ namespace smt {
         return true;
     }
 
+    bool theory_jobscheduler::internalize_atom(app * atom, bool gate_ctx) {
+        SASSERT(u.is_model(atom));
+        for (expr* arg : *atom) {
+            internalize_cmd(arg);
+        }
+        add_done();
+        return true;
+    }
+
+    // TBD: stronger parameter validation
+    void theory_jobscheduler::internalize_cmd(expr* cmd) {
+        symbol key, val;
+        rational r;
+        if (u.is_kv(cmd, key, r)) {
+            if (key == ":set-preemptable" && r.is_unsigned()) {
+                set_preemptable(r.get_unsigned(), true);
+                return;
+            }
+            warning_msg("command not recognized");
+        }
+        else if (u.is_alist(cmd, key) && key == ":add-job-resource") {
+            properties ps;
+            unsigned j = 0, res = 0, cap = 0, loadpct = 100;
+            time_t end = std::numeric_limits<time_t>::max();
+            for (expr* arg : *to_app(cmd)) {
+                if (u.is_kv(arg, key, r)) {
+                    if (key == ":job") {
+                        j = r.get_unsigned();
+                    }
+                    else if (key == ":resource") {
+                        res = r.get_unsigned();
+                    }
+                    else if (key == ":capacity") {
+                        cap = r.get_unsigned();
+                    }
+                    else if (key == ":loadpct") {
+                        loadpct = r.get_unsigned();
+                    }
+                    else if (key == ":end") {
+                        end = r.get_uint64();
+                    }
+                }
+                else if (u.is_alist(arg, key) && key == ":properties") {
+                    // TBD
+                }
+            }
+            if (cap > 0) {
+                add_job_resource(j, res, cap, loadpct, end, ps);
+            }
+            else {
+                warning_msg("no job capacity provided");
+            }
+        }
+        else if (u.is_alist(cmd, key) && key == ":add-resource-available") {
+            properties ps;
+            unsigned res = 0, loadpct = 100;
+            time_t start = 0, end = 0;
+            for (expr* arg : *to_app(cmd)) {
+                if (u.is_kv(arg, key, r)) {
+                    if (key == ":resource") {
+                        res = r.get_unsigned();
+                    }
+                    else if (key == ":start") {
+                        start = r.get_unsigned();
+                    }
+                    else if (key == ":end") {
+                        end = r.get_unsigned();
+                    }
+                    else if (key == ":loadpct") {
+                        loadpct = r.get_unsigned();
+                    }
+                }
+                else if (u.is_alist(arg, key) && key == ":properties") {
+                    // TBD
+                }
+                add_resource_available(res, loadpct, start, end, ps);
+            }
+            
+        }
+        else {
+            warning_msg("command not recognized");
+        }
+    }
 
     void theory_jobscheduler::push_scope_eh() {
     }
@@ -214,7 +297,7 @@ namespace smt {
             if (ctx.get_assignment(start_ge_lo) != l_true) {
                 return;
             }
-            enode_pair eq(ji.m_resource, ctx.get_enode(u.mk_resource(r)));
+            enode_pair eq(ji.m_job2resource, resource2enode(r));
             if (eq.first->get_root() != eq.second->get_root()) {
                 return;
             }
@@ -368,7 +451,7 @@ namespace smt {
     }
         
     theory_jobscheduler::theory_jobscheduler(ast_manager& m): 
-        theory(m.get_family_id("jobshop")), m(m), u(m), a(m) {
+        theory(m.get_family_id("csp")), m(m), u(m), a(m) {
     }
 
     std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const {
@@ -423,51 +506,76 @@ namespace smt {
         return alloc(theory_jobscheduler, new_ctx->get_manager()); 
     }
 
-    time_t theory_jobscheduler::est(unsigned j) {
+    time_t theory_jobscheduler::get_lo(expr* e) {
         arith_value av(get_context());
         rational val;
         bool is_strict;
-        if (av.get_lo(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
+        if (av.get_lo(e, val, is_strict) && !is_strict && val.is_uint64()) {
             return val.get_uint64();
         }
         return 0;
     }
 
-    time_t theory_jobscheduler::lst(unsigned j) {
+    time_t theory_jobscheduler::get_up(expr* e) {
         arith_value av(get_context());
         rational val;
         bool is_strict;
-        if (av.get_up(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
+        if (av.get_up(e, val, is_strict) && !is_strict && val.is_uint64()) {
             return val.get_uint64();
         }
         return std::numeric_limits<time_t>::max();
     }
 
-    time_t theory_jobscheduler::ect(unsigned j) {
-        NOT_IMPLEMENTED_YET();
+    time_t theory_jobscheduler::get_value(expr* e) {
+        arith_value av(get_context());
+        rational val;
+        if (av.get_value(e, val) && val.is_uint64()) {
+            return val.get_uint64();
+        }
         return 0;
+    }    
+
+    time_t theory_jobscheduler::est(unsigned j) {
+        return get_lo(m_jobs[j].m_start->get_owner());
+    }
+
+    time_t theory_jobscheduler::lst(unsigned j) {
+        return get_up(m_jobs[j].m_start->get_owner());
+    }
+
+    time_t theory_jobscheduler::ect(unsigned j) {
+        return get_lo(m_jobs[j].m_end->get_owner());
     }
 
     time_t theory_jobscheduler::lct(unsigned j) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        return get_up(m_jobs[j].m_end->get_owner());
     }
 
     time_t theory_jobscheduler::start(unsigned j) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        return get_value(m_jobs[j].m_start->get_owner());
     }
 
     time_t theory_jobscheduler::end(unsigned j) {
-        NOT_IMPLEMENTED_YET();
-        return 0;
+        return get_value(m_jobs[j].m_end->get_owner());
     }
 
     unsigned theory_jobscheduler::resource(unsigned j) {
-        NOT_IMPLEMENTED_YET();
+        unsigned r;
+        enode* next = m_jobs[j].m_job2resource, *n = next;
+        do {
+            if (u.is_resource(next->get_owner(), r)) {
+                return r;
+            }
+            next = next->get_next();
+        }
+        while (next != n);
         return 0;
     }
 
+    enode* theory_jobscheduler::resource2enode(unsigned r) {
+        return get_context().get_enode(u.mk_resource(r));
+    }
+
     void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) {
         m_jobs.reserve(j + 1);
         m_jobs[j].m_is_preemptable = is_preemptable;        
@@ -494,7 +602,8 @@ namespace smt {
         SASSERT(1 <= max_loadpct && max_loadpct <= 100);
         SASSERT(start <= end);
         m_resources.reserve(r + 1);
-        m_resources[r].m_available.push_back(res_available(max_loadpct, start, end, ps));
+        res_info& ri = m_resources[r];
+        ri.m_available.push_back(res_available(max_loadpct, start, end, ps));
     }
 
     /*
diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h
index 117303ff7..3647e6a1b 100644
--- a/src/smt/theory_jobscheduler.h
+++ b/src/smt/theory_jobscheduler.h
@@ -62,8 +62,8 @@ namespace smt {
             u_map<unsigned>      m_resource2index; // resource to index into vector 
             enode*               m_start;
             enode*               m_end;
-            enode*               m_resource;
-            job_info(): m_is_preemptable(true), m_start(nullptr), m_end(nullptr), m_resource(nullptr) {}
+            enode*               m_job2resource;
+            job_info(): m_is_preemptable(false), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr) {}
         };
 
         struct res_available {
@@ -88,7 +88,8 @@ namespace smt {
             unsigned_vector       m_jobs;      // jobs allocated to run on resource
             vector<res_available> m_available; // time intervals where resource is available
             time_t                m_end;       // can't run after
-            res_info(): m_end(std::numeric_limits<time_t>::max()) {}
+            enode*                m_resource;
+            res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr) {}
         };
         
         ast_manager&     m;
@@ -102,7 +103,7 @@ namespace smt {
 
         theory_var mk_var(enode * n) override;        
 
-        bool internalize_atom(app * atom, bool gate_ctx) override { return false; }
+        bool internalize_atom(app * atom, bool gate_ctx) override;
 
         bool internalize_term(app * term) override;
 
@@ -154,7 +155,11 @@ namespace smt {
         time_t lct(unsigned j);      // last completion time
         time_t start(unsigned j);    // start time of job j
         time_t end(unsigned j);      // end time of job j
+        time_t get_lo(expr* e);
+        time_t get_up(expr* e);
+        time_t get_value(expr* e);
         unsigned resource(unsigned j); // resource of job j
+        enode* resource2enode(unsigned r);
 
         // derived bounds
         time_t ect(unsigned j, unsigned r, time_t start);
@@ -201,6 +206,8 @@ namespace smt {
         literal mk_le(enode* l, enode* r);
         literal mk_literal(expr* e);
 
+        void internalize_cmd(expr* cmd);
+
         std::ostream& display(std::ostream & out, res_info const& r) const;
         std::ostream& display(std::ostream & out, res_available const& r) const;
         std::ostream& display(std::ostream & out, job_info const& r) const;
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 59a9a1562..d0fd8f809 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -22,7 +22,7 @@ Revision History:
 
 
 bool smt_logics::supported_logic(symbol const & s) {
-    return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) ||
+    return logic_has_uf(s) || logic_is_allcsp(s) || logic_has_fd(s) || 
         logic_has_arith(s) || logic_has_bv(s) ||
         logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
         logic_has_horn(s) || logic_has_fpa(s);
@@ -83,7 +83,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
         s == "QF_S" ||
-        s == "ALL" ||
+        logic_is_allcsp(s) ||
         s == "QF_FD" ||
         s == "HORN" ||
         s == "QF_FPLRA";
@@ -102,7 +102,7 @@ bool smt_logics::logic_has_bv(symbol const & s) {
         s == "QF_BVRE" ||
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
-        s == "ALL" ||
+        logic_is_allcsp(s) ||
         s == "QF_FD" ||
         s == "HORN";
 }
@@ -123,22 +123,22 @@ bool smt_logics::logic_has_array(symbol const & s) {
         s == "AUFNIRA" ||
         s == "AUFBV" ||
         s == "ABV" ||
-        s == "ALL" ||
+        logic_is_allcsp(s) ||
         s == "QF_ABV" ||
         s == "QF_AUFBV" ||
         s == "HORN";
 }
 
 bool smt_logics::logic_has_seq(symbol const & s) {
-    return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
+    return s == "QF_BVRE" || s == "QF_S" || logic_is_allcsp(s);
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || s == "ALL";
+    return s == "QF_S" || logic_is_allcsp(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {
-    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || s == "ALL";
+    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || logic_is_allcsp(s);
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
@@ -150,9 +150,10 @@ bool smt_logics::logic_has_horn(symbol const& s) {
 }
 
 bool smt_logics::logic_has_pb(symbol const& s) {
-    return s == "QF_FD" || s == "ALL" || logic_has_horn(s);
+    return s == "QF_FD" || logic_is_allcsp(s) || logic_has_horn(s);
 }
 
 bool smt_logics::logic_has_datatype(symbol const& s) {
-    return s == "QF_FD" || s == "ALL" || s == "QF_DT";
+    return s == "QF_FD" || logic_is_allcsp(s) || s == "QF_DT";
 }
+
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
index 702431cdd..4382f575b 100644
--- a/src/solver/smt_logics.h
+++ b/src/solver/smt_logics.h
@@ -25,6 +25,8 @@ public:
     static bool supported_logic(symbol const & s);
     static bool logic_has_reals_only(symbol const& l);       
     static bool logic_is_all(symbol const& s) { return s == "ALL"; }
+    static bool logic_is_csp(symbol const& s) { return s == "CSP"; }
+    static bool logic_is_allcsp(symbol const& s) { return logic_is_all(s) || logic_is_csp(s); }
     static bool logic_has_uf(symbol const& s);
     static bool logic_has_arith(symbol const & s);
     static bool logic_has_bv(symbol const & s);