Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.

I also expect this commit to fix bug #273.

No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863

2 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index ae37dfe99..03787703a 100644
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 using namespace CVC4::theory::uf::tim;
 
-TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
-  TheoryUF(c, out, valuation),
+TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_UF, c, u, out, valuation),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h
index 70c60728f..b47536f07 100644
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -43,7 +43,7 @@ namespace theory {
 namespace uf {
 namespace tim {
 
-class TheoryUFTim : public TheoryUF {
+class TheoryUFTim : public Theory {
 
 private:
 
@@ -85,7 +85,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation);
+  TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUFTim();