diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 09f082522..aea8863af 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -361,6 +361,9 @@ public:
     app * mk_int(int i) {
         return mk_numeral(rational(i), true);
     }
+    app * mk_int(rational const& r) {
+        return mk_numeral(r, true);
+    }
     app * mk_real(int i) {
         return mk_numeral(rational(i), false);
     }
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index f8439917e..d2cab8bf8 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -89,12 +89,41 @@ namespace smt {
         
     }
         
-    theory_jobscheduler::theory_jobscheduler(ast_manager& m): theory(m.get_family_id("jobshop")), m(m), u(m) {
+    theory_jobscheduler::theory_jobscheduler(ast_manager& m): 
+        theory(m.get_family_id("jobshop")), m(m), u(m), a(m) {
 
     }
-        
-    void theory_jobscheduler::display(std::ostream & out) const {
 
+    std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const {
+        return out << "   r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end << "\n";
+    }
+
+    std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const {
+        for (job_resource const& jr : j.m_resources) {
+            display(out, jr);
+        }
+        return out;
+    }
+
+    std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const {
+        out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%%\n";
+        return out;
+    }
+
+    std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const {
+        for (res_available const& ra : r.m_available) {
+            display(out, ra);
+        }
+        return out;
+    }
+
+    void theory_jobscheduler::display(std::ostream & out) const {
+        for (unsigned j = 0; j < m_jobs.size(); ++j) {
+            display(out << "job " << j << ":\n", m_jobs[j]);
+        }
+        for (unsigned r = 0; r < m_resources.size(); ++r) {
+            display(out << "resource " << r << ":\n", m_resources[r]);
+        }
     }
         
     void theory_jobscheduler::collect_statistics(::statistics & st) const {
@@ -117,27 +146,27 @@ namespace smt {
         return alloc(theory_jobscheduler, new_ctx->get_manager()); 
     }
 
-    uint64_t theory_jobscheduler::est(unsigned j) {
+    time_t theory_jobscheduler::est(unsigned j) {
         return 0;
     }
 
-    uint64_t theory_jobscheduler::lst(unsigned j) {
+    time_t theory_jobscheduler::lst(unsigned j) {
         return 0;
     }
 
-    uint64_t theory_jobscheduler::ect(unsigned j) {
+    time_t theory_jobscheduler::ect(unsigned j) {
         return 0;
     }
 
-    uint64_t theory_jobscheduler::lct(unsigned j) {
+    time_t theory_jobscheduler::lct(unsigned j) {
         return 0;
     }
 
-    uint64_t theory_jobscheduler::start(unsigned j) {
+    time_t theory_jobscheduler::start(unsigned j) {
         return 0;
     }
 
-    uint64_t theory_jobscheduler::end(unsigned j) {
+    time_t theory_jobscheduler::end(unsigned j) {
         return 0;
     }
 
@@ -146,8 +175,8 @@ namespace smt {
     }
 
 
-    void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, uint64_t end) {
-        // assert: done at base level
+    void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end) {
+        SASSERT(get_context().at_base_level());
         m_jobs.reserve(j + 1);
         m_resources.reserve(r + 1);
         job_info& ji = m_jobs[j];
@@ -160,12 +189,189 @@ namespace smt {
         m_resources[r].m_jobs.push_back(j);
     }
 
-    void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, uint64_t start, uint64_t end) {
-        // assert: done at base level
+    void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end) {
+        SASSERT(get_context().at_base_level());
         SASSERT(start < end);
         m_resources.reserve(r + 1);
         m_resources[r].m_available.push_back(res_available(max_loadpct, start, end));
     }
+
+    /*
+     * Initialze the state based on the set of jobs and resources added.
+     * For each job j, with possible resources r1, ..., r_n assert
+     *   resource(j) = r_1 || resource(j) = r_2 || ... || resource(j) = r_n
+     * For each job and resource r with deadline end(j,r) assert
+     *   resource(j) = r => end(j) <= end(j,r)
+     *
+     * Ensure that the availability slots for each resource is sorted by time.
+     */
+    void theory_jobscheduler::add_done() {
+        context & ctx = get_context();        
+        for (unsigned j = 0; j < m_jobs.size(); ++j) {
+            job_info const& ji = m_jobs[j];
+            expr_ref_vector disj(m);
+            app_ref job(u.mk_job(j), m);
+            if (ji.m_resources.empty()) {
+                throw default_exception("every job should be associated with at least one resource");
+            }
+            // resource(j) = r => end(j) <= end(j, r)
+            for (job_resource const& jr : ji.m_resources) {
+                app_ref res(u.mk_resource(jr.m_resource_id), m);
+                expr_ref eq(m.mk_eq(job, res), m);
+                expr_ref imp(m.mk_implies(eq, a.mk_le(ji.m_start->get_owner(), a.mk_int(rational(jr.m_end, rational::ui64())))), m);
+                ctx.assert_expr(imp);                
+                disj.push_back(eq);
+            }
+            // resource(j) = r1 || ... || resource(j) = r_n
+            expr_ref fml = mk_or(disj);
+            ctx.assert_expr(fml);
+        }        
+        for (unsigned r = 0; r < m_resources.size(); ++r) {
+            vector<res_available>& available = m_resources[r].m_available;
+            res_available::compare cmp;
+            std::sort(available.begin(), available.end(), cmp);
+            for (unsigned i = 0; i < available.size(); ++i) {
+                if (i + 1 < available.size() &&
+                    available[i].m_end > available[i + 1].m_start) {
+                    throw default_exception("availability intervals should be disjoint");
+                }
+            }
+        }
+    }
+
+    /**
+     * check that each job is run on some resource according to 
+     * requested capacity.
+     * 
+     * Check that the sum of jobs run in each time instance
+     * does not exceed capacity.
+     */
+    void theory_jobscheduler::validate_assignment() {
+        vector<vector<job_time>> start_times, end_times;
+        start_times.reserve(m_resources.size());
+        end_times.reserve(m_resources.size());
+        for (unsigned j = 0; j < m_jobs.size(); ++j) {
+            unsigned r = resource(j);
+            start_times[r].push_back(job_time(j, start(j))); 
+            end_times[r].push_back(job_time(j, end(j))); 
+            time_t cap = capacity_used(j, r, start(j), end(j));
+            job_resource const& jr = get_job_resource(j, r);
+            if (jr.m_capacity > cap) {
+                throw default_exception("job not assigned full capacity");
+            }
+        }
+        for (unsigned r = 0; r < m_resources.size(); ++r) {
+            unsigned load_pct = 0;
+            unsigned idx;
+            time_t next = 0, start = 0;
+
+            // order jobs running on r by start, end-time intervals
+            // then consume ordered list to find jobs in scope.
+            vector<job_time>& starts = start_times[r];
+            vector<job_time>& ends = end_times[r];
+            job_time::compare cmp;
+            std::sort(starts.begin(), starts.end(), cmp);
+            std::sort(ends.begin(),   ends.end(),   cmp);
+            unsigned s_idx = 0, e_idx = 0;
+
+            uint_set jobs; // set of jobs currently in scope.
+            while (resource_available(r, start, load_pct, next, idx)) {
+                if (load_pct == 0) {
+                    start = next + 1;
+                    continue;
+                }
+                // add jobs that begin at or before start.
+                while (s_idx < starts.size() && starts[s_idx].m_time <= start) {
+                    jobs.insert(starts[s_idx].m_job);
+                    ++s_idx;
+                }
+                // remove jobs that end before start.
+                while (e_idx < ends.size() && ends[s_idx].m_time < start) {
+                    jobs.remove(ends[e_idx].m_job);
+                    ++e_idx;
+                }
+
+                // check that sum of job loads does not exceed 100%
+                unsigned cap = 0;
+                for (auto j : jobs) {
+                    cap += get_job_resource(j, r).m_loadpct;
+                }
+                if (cap > 100) {
+                    throw default_exception("capacity on resource exceeded");
+                }
+                if (s_idx < starts.size()) {
+                    // start time of the next unprocessed job.
+                    start = starts[s_idx].m_time;
+                }
+                else {
+                    // done checking.
+                    break;
+                }
+            }
+        }
+    }
+
+    theory_jobscheduler::job_resource const& theory_jobscheduler::get_job_resource(unsigned j, unsigned r) const {
+        job_info const& ji = m_jobs[j];
+        return ji.m_resources[ji.m_resource2index[r]];
+    }
+
+    bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& load_pct, time_t& end, unsigned& idx) {
+        vector<res_available>& available = m_resources[r].m_available;
+        unsigned lo = 0, hi = available.size(), mid = hi / 2;
+        while (lo < hi) {
+            res_available const& ra = available[mid];
+            if (ra.m_start <= t && t <= ra.m_end) {
+                end = ra.m_end;
+                load_pct = ra.m_loadpct;
+                idx = mid;
+                return true;
+            }
+            else if (ra.m_start > t && mid > 0) {
+                hi = mid - 1;
+                mid = lo + (mid - lo) / 2;
+            }
+            else if (ra.m_end < t) {
+                lo = mid + 1;
+                mid += (hi - mid) / 2;
+            }
+            else {
+                break;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * compute the capacity used by job j on resource r between start and end.
+     * The resource r partitions time intervals into segments where a fraction of
+     * the full capacity of the resource is available. The resource can use up to the
+     * available fraction.
+     */
+    time_t theory_jobscheduler::capacity_used(unsigned j, unsigned r, time_t start, time_t end) {
+        time_t cap = 0;
+        unsigned j_load_pct = get_job_resource(j, r).m_loadpct;
+        vector<res_available>& available = m_resources[r].m_available;
+        unsigned load_pct = 0;
+        time_t next = 0;
+        unsigned idx = 0;
+        if (!resource_available(r, start, load_pct, next, idx)) {
+            return cap;
+        }
+        while (start < end) {
+            next = std::min(end, next);
+            SASSERT(start < next);
+            cap += (std::min(j_load_pct, load_pct) / j_load_pct) * (next - start - 1);
+            ++idx;
+            if (idx == available.size()) {
+                break;
+            }
+            start = available[idx].m_start;
+            next  = available[idx].m_end;
+            load_pct = available[idx].m_loadpct;
+        }        
+        return cap;
+    }
     
 };
 
diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h
index ec09ce0ce..f10b72d81 100644
--- a/src/smt/theory_jobscheduler.h
+++ b/src/smt/theory_jobscheduler.h
@@ -22,20 +22,35 @@ Revision History:
 
 #include "smt/smt_theory.h"
 #include "ast/jobshop_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
 
 namespace smt {
 
+    typedef uint64_t time_t;
+
     class theory_jobscheduler : public theory {
 
         struct job_resource {
             unsigned m_resource_id;   // id of resource
             unsigned m_capacity;      // amount of resource to use
             unsigned m_loadpct;       // assuming loadpct
-            uint64_t m_end;           // must run before
-            job_resource(unsigned r, unsigned cap, unsigned loadpct, uint64_t end):
+            time_t   m_end;           // must run before
+            job_resource(unsigned r, unsigned cap, unsigned loadpct, time_t end):
                 m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end) {}
         };
 
+        struct job_time {
+            unsigned m_job;
+            time_t   m_time;
+            job_time(unsigned j, time_t time): m_job(j), m_time(time) {}
+
+            struct compare {
+                bool operator()(job_time const& jt1, job_time const& jt2) const {
+                    return jt1.m_time < jt2.m_time;
+                }
+            };
+        };
+
         struct job_info {
             vector<job_resource> m_resources; // resources allowed to run job.
             u_map<unsigned>      m_resource2index; // resource to index into vector 
@@ -47,24 +62,31 @@ namespace smt {
 
         struct res_available {
             unsigned m_loadpct;
-            uint64_t m_start;
-            uint64_t m_end;
-            res_available(unsigned load_pct, uint64_t start, uint64_t end):
+            time_t m_start;
+            time_t m_end;
+            res_available(unsigned load_pct, time_t start, time_t end):
                 m_loadpct(load_pct),
                 m_start(start),
                 m_end(end)
             {}
+            struct compare {
+                bool operator()(res_available const& ra1, res_available const& ra2) const {
+                    return ra1.m_start < ra2.m_start;
+                }
+            };
+
         };
 
         struct res_info {
             unsigned_vector       m_jobs;      // jobs allocated to run on resource
             vector<res_available> m_available; // time intervals where resource is available
-            uint64_t              m_end;       // can't run after
-            res_info(): m_end(std::numeric_limits<uint64_t>::max()) {}
+            time_t              m_end;       // can't run after
+            res_info(): m_end(std::numeric_limits<time_t>::max()) {}
         };
         
         ast_manager&     m;
         jobshop_util     u;
+        arith_util       a;
         unsigned_vector  m_var2index;
         vector<job_info> m_jobs;
         vector<res_info> m_resources;
@@ -113,17 +135,31 @@ namespace smt {
 
     public:
         // assignments:
-        uint64_t est(unsigned j);      // earliest start time of job j
-        uint64_t lst(unsigned j);      // last start time
-        uint64_t ect(unsigned j);      // earliest completion time
-        uint64_t lct(unsigned j);      // last completion time
-        uint64_t start(unsigned j);    // start time of job j
-        uint64_t end(unsigned j);      // end time of job j
+        time_t est(unsigned j);      // earliest start time of job j
+        time_t lst(unsigned j);      // last start time
+        time_t ect(unsigned j);      // earliest completion time
+        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
         unsigned resource(unsigned j); // resource of job j
         
         // set up model
-        void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, uint64_t end);
-        void add_resource_available(unsigned r, unsigned max_loadpct, uint64_t start, uint64_t end);
+        void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end);
+        void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end);
+        void add_done();
+
+        // validate assignment
+        void validate_assignment();
+        bool resource_available(unsigned r, time_t t, unsigned& load_pct, time_t& end, unsigned& idx); // load available on resource r at time t.
+        time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end);        // capacity used between start and end
+
+        job_resource const& get_job_resource(unsigned j, unsigned r) const;
+
+        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;
+        std::ostream& display(std::ostream & out, job_resource const& r) const;
+
     };    
 };