From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 3 Jan 2014 18:13:13 +0000 (-0600)
Subject: Added support for proof production in Equality Engine.  Cleaned up existing proof... 
X-Git-Tag: cvc5-1.0.0~7168
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93f084750d8a76d63fc74d242944bce0635c2194;p=cvc5.git

Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.
---

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 67ce3988a..bbee2d49b 100755
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -3,15 +3,14 @@
 ; SMT syntax and semantics (not theory-specific)
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on sat.plf
 
 (declare formula type)
 (declare th_holds (! f formula type))
 
-; constants
+; standard logic definitions
 (declare true formula)
 (declare false formula)
-
-; logical connectives
 (declare not (! f formula formula))
 (declare and (! f1 formula (! f2 formula formula)))
 (declare or (! f1 formula (! f2 formula formula)))
@@ -21,24 +20,19 @@
 (declare ifte (! b formula (! f1 formula (! f2 formula formula))))
 
 ; terms
-(declare sort type)				; sort in the theory
-(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
-
+(declare sort type)
 (declare term (! t sort type))	; declared terms in formula
 
-(declare apply (! s1 sort
-               (! s2 sort
-               (! t1 (term (arrow s1 s2))
-               (! t2 (term s1)
-                (term s2))))))
-
+; standard definitions for =, ite, let and flet
+(declare = (! s sort
+           (! x (term s)
+           (! y (term s)
+             formula))))
 (declare ite (! s sort
              (! f formula
              (! t1 (term s)
              (! t2 (term s)
                (term s))))))
-
-; let/flet
 (declare let (! s sort
              (! t (term s)
              (! f (! v (term s) formula)
@@ -47,38 +41,52 @@
               (! f2 (! v formula formula)
                 formula)))
 
-; predicates
-(declare = (! s sort
-           (! x (term s)
-           (! y (term s)
-             formula))))
-
-; To avoid duplicating some of the rules (e.g., cong), we will view
-; applications of predicates as terms of sort "Bool".
+; We view applications of predicates as terms of sort "Bool".
 ; Such terms can be injected as atomic formulas using "p_app".
-
 (declare Bool sort)				; the special sort for predicates
 (declare p_app (! x (term Bool) formula))	; propositional application of term
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; Examples
+;
+; CNF Clausification
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; an example of "(p1 or p2(0)) and t1=t2(1)"
-;(! p1 (term Bool)
-;(! p2 (term (arrow Int Bool))
-;(! t1 (term Int)
-;(! t2 (term (arrow Int Int))
-;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
-;                    (= _ t1 (apply _ _ t2 1))))
-;  ...
+; binding between an LF var and an (atomic) formula
+(declare atom (! v var (! p formula type)))
 
-; another example of "p3(a,b)"
-;(! a (term Int)
-;(! b (term Int)
-;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
-;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
-;  ...
+(declare decl_atom
+  (! f formula
+  (! u (! v var
+       (! a (atom v f)
+         (holds cln)))
+    (holds cln))))
+
+; clausify a formula directly
+(declare clausify_form
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds f)
+    (holds (clc (pos v) cln)))))))
+    
+(declare clausify_form_not
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds (not f))
+    (holds (clc (neg v) cln)))))))
+    
+(declare clausify_false
+  (! u (th_holds false)
+    (holds cln)))
+
+(declare th_let_pf
+  (! f formula
+  (! u (th_holds f)
+  (! u2 (! v (th_holds f) (holds cln))
+    (holds cln)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -261,13 +269,41 @@
   (! u2 (th_holds (not (ifte (not a) b c)))
     (th_holds (not c))))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; For theory lemmas
+; - make a series of assumptions and then derive a contradiction (or false)
+; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
+; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare ast
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)       ;this is specified
+  (! u (! o (th_holds f)
+         (holds C))
+    (holds (clc (neg v) C))))))))
+
+(declare asf
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)
+  (! u (! o (th_holds (not f))
+         (holds C))
+    (holds (clc (pos v) C))))))))
+    
+
 
 
-;; How to do CNF for disjunctions of theory literals.
+;; Example:
 ;;
-;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
+;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
 ;;
-;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
+;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn).
 ;; Do this at the beginning of the proof:
 ;;
 ;; (decl_atom F1 (\ v1 (\ a1
@@ -275,7 +311,7 @@
 ;; ....
 ;; (decl_atom Fn (\ vn (\ an
 ;;
-;; Our input A is clausified by the following proof:
+;;  A is then clausified by the following proof:
 ;;
 ;;(satlem _ _
 ;;(asf _ _ _ a1 (\ l1
@@ -294,7 +330,7 @@
 ;;
 ;; We now have the free variable C, which should be the clause (v1 V ... V vn).
 ;;
-;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
+;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
 ;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
 ;; the arguments of contra:
 ;;
@@ -311,3 +347,5 @@
 ;;))))))) (\ C
 ;;
 ;; C should be the clause (~v1 V v2 V ~v3 )
+
+
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
new file mode 100755
index 000000000..6e0e6438d
--- /dev/null
+++ b/proofs/signatures/th_arrays.plf
@@ -0,0 +1,53 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Arrays
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depdends on : th_base.plf
+
+; sorts
+
+(declare array (! s1 sort (! s2 sort sort)))	; s1 is index, s2 is element
+
+; functions
+(declare write (! s1 sort
+               (! s2 sort
+               (! t1 (term (array s1 s2))
+               (! t2 (term s1)
+               (! t3 (term s2)
+                (term (array s1 s2))))))))
+(declare read (! s1 sort
+              (! s2 sort
+              (! t1 (term (array s1 s2))
+              (! t2 (term s1)
+                (term s2))))))
+                
+; inference rules
+(declare row1 (! s1 sort
+              (! s2 sort
+              (! t1 (term (array s1 s2))
+              (! t2 (term s1)
+              (! t3 (term s2)
+              	(th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
+              	
+
+(declare row (! s1 sort
+             (! s2 sort
+             (! t1 (term (array s1 s2))
+             (! t2 (term s1)
+             (! t3 (term s1)
+             (! t4 (term s2)
+             (! u (th_holds (not (= _ t2 t3)))
+               (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
+
+(declare ext (! s1 sort
+             (! s2 sort
+             (! f formula
+             (! t1 (term (array s1 s2))
+             (! t2 (term (array s1 s2))
+             (! u (th_holds (not (= _ t1 t2)))
+             (! u1 (! k (term s1)
+                   (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
+                     (th_holds f)))
+               (th_holds f)))))))))
+               
\ No newline at end of file
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index 7b0b086dc..977409b6a 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -1,80 +1,28 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization / Clausification
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; binding between an LF var and an (atomic) formula
-(declare atom (! v var (! p formula type)))
-
-(declare decl_atom
-  (! f formula
-  (! u (! v var
-       (! a (atom v f)
-         (holds cln)))
-    (holds cln))))
-
-; direct clausify
-(declare clausify_form
-  (! f formula
-  (! v var
-  (! a (atom v f)
-  (! u (th_holds f)
-    (holds (clc (pos v) cln)))))))
-
-(declare clausify_form_not
-  (! f formula
-  (! v var
-  (! a (atom v f)
-  (! u (th_holds (not f))
-    (holds (clc (neg v) cln)))))))
-
-(declare clausify_false
-  (! u (th_holds false)
-    (holds cln)))
 
 
-(declare th_let_pf
-  (! f formula
-  (! u (th_holds f)
-  (! u2 (! v (th_holds f) (holds cln))
-    (holds cln)))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
-; Theory reasoning
-; - make a series of assumptions and then derive a contradiction (or false)
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+; Theory of Equality and Congruence Closure
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on : smt.plf
 
-(declare ast
-  (! v var
-  (! f formula
-  (! C clause
-  (! r (atom v f)       ;this is specified
-  (! u (! o (th_holds f)
-         (holds C))
-    (holds (clc (neg v) C))))))))
+; sorts :
 
-(declare asf
-  (! v var
-  (! f formula
-  (! C clause
-  (! r (atom v f)
-  (! u (! o (th_holds (not f))
-         (holds C))
-    (holds (clc (pos v) C))))))))
+(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; functions :
 
-; temporary :
-(declare trust (th_holds false))
+(declare apply (! s1 sort
+               (! s2 sort
+               (! t1 (term (arrow s1 s2))
+               (! t2 (term s1)
+                (term s2))))))
+                
+                
+; inference rules :
+
+(declare trust (th_holds false))	; temporary
 
 (declare refl
   (! s sort
@@ -105,3 +53,21 @@
               (! u2 (th_holds (= _ a2 b2))
                 (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Examples
+
+; an example of "(p1 or p2(0)) and t1=t2(1)"
+;(! p1 (term Bool)
+;(! p2 (term (arrow Int Bool))
+;(! t1 (term Int)
+;(! t2 (term (arrow Int Int))
+;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
+;                    (= _ t1 (apply _ _ t2 1))))
+;  ...
+
+; another example of "p3(a,b)"
+;(! a (term Int)
+;(! b (term Int)
+;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
+;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
+;  ...
diff --git a/src/Makefile.am b/src/Makefile.am
index c765d325a..eda6acd6b 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -291,6 +291,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/relevant_domain.cpp \
 	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/symmetry_breaking.cpp \
+	theory/quantifiers/qinterval_builder.h \
+	theory/quantifiers/qinterval_builder.cpp \
 	theory/quantifiers/options_handlers.h \
 	theory/rewriterules/theory_rewriterules_rules.h \
 	theory/rewriterules/theory_rewriterules_rules.cpp \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f26456cae..539622877 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -771,7 +771,7 @@ void SmtEngine::finishInit() {
     setTimeLimit(options::cumulativeMillisecondLimit(), true);
   }
 
-  PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); 
+  PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
 }
 
 void SmtEngine::finalOptionsAreSet() {
@@ -1144,13 +1144,17 @@ void SmtEngine::setLogicInternal() throw() {
   }
   if ( ! options::fmfInstGen.wasSetByUser()) {
     //if full model checking is on, disable inst-gen techniques
-    if( options::fmfFullModelCheck() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
       options::fmfInstGen.set( false );
+    }else{
+      options::fmfInstGen.set( true );
     }
   }
   if ( options::fmfBoundInt() ){
-    //if bounded integers are set, must use full model check for MBQI
-    options::fmfFullModelCheck.set( true );
+    if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
+      //if bounded integers are set, must use full model check for MBQI
+      options::mbqiMode.set( quantifiers::MBQI_FMC );
+    }
   }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
@@ -3309,7 +3313,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
     // Ensure expr is type-checked at this point.
     ensureBoolean(e);
     // Give it to proof manager
-    PROOF( ProofManager::currentPM()->addAssertion(e); ); 
+    PROOF( ProofManager::currentPM()->addAssertion(e); );
   }
 
   // check to see if a postsolve() is pending
@@ -3390,7 +3394,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
   // Give it to proof manager
-  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); 
+  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); );
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3455,7 +3459,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   finalOptionsAreSet();
   doPendingPops();
 
-  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
+  PROOF( ProofManager::currentPM()->addAssertion(ex); );
 
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index bda124e96..c94775aec 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/qinterval_builder.h"
 
 #define USE_INDEX_ORDERING
 
@@ -27,8 +29,9 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::quantifiers::fmcheck;
 
-FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
-d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
+FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
+TheoryModel( c, name, true ),
+d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
 
 }
 
@@ -66,16 +69,23 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
 }
 
 void FirstOrderModel::initialize( bool considerAxioms ) {
-  processInitialize();
+  processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
   for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
     Node f = getAssertedQuantifier( i );
+    processInitializeQuantifier( f );
+    if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
+      for(unsigned i=0; i<f[0].getNumChildren(); i++){
+        d_quant_var_id[f][f[0][i]] = i;
+      }
+    }
     if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){
       //initialize relevant models within bodies of all quantifiers
       initializeModelForTerm( f[1] );
     }
   }
+  processInitialize( false );
 }
 
 void FirstOrderModel::initializeModelForTerm( Node n ){
@@ -85,14 +95,30 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
   }
 }
 
-FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) {
+Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
+  //check if there is even any domain elements at all
+  if (!d_rep_set.hasType(tn)) {
+    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    d_rep_set.add(mbt);
+  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
+    Message() << "empty reps" << std::endl;
+    exit(0);
+  }
+  return d_rep_set.d_type_reps[tn][0];
+}
+
+FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(qe, c,name) {
 
 }
 
-void FirstOrderModelIG::processInitialize(){
-  //rebuild models
-  d_uf_model_tree.clear();
-  d_uf_model_gen.clear();
+void FirstOrderModelIG::processInitialize( bool ispre ){
+  if( ispre ){
+    //rebuild models
+    d_uf_model_tree.clear();
+    d_uf_model_gen.clear();
+  }
 }
 
 void FirstOrderModelIG::processInitializeModelForTerm( Node n ){
@@ -513,10 +539,8 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar
 
 
 
-
-
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(c, name), d_qe(qe){
+FirstOrderModel(qe, c, name){
 
 }
 
@@ -552,19 +576,21 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
   return d_models[n.getOperator()]->evaluate(this, args);
 }
 
-void FirstOrderModelFmc::processInitialize() {
-  if( options::fmfFmcInterval() && intervalOp.isNull() ){
-    std::vector< TypeNode > types;
-    for(unsigned i=0; i<2; i++){
-      types.push_back(NodeManager::currentNM()->integerType());
+void FirstOrderModelFmc::processInitialize( bool ispre ) {
+  if( ispre ){
+    if( options::fmfFmcInterval() && intervalOp.isNull() ){
+      std::vector< TypeNode > types;
+      for(unsigned i=0; i<2; i++){
+        types.push_back(NodeManager::currentNM()->integerType());
+      }
+      TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
+      intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
     }
-    TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
-    intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
-  }
-  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
-    it->second->reset();
+    for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+      it->second->reset();
+    }
+    d_model_basis_rep.clear();
   }
-  d_model_basis_rep.clear();
 }
 
 void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
@@ -575,19 +601,6 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
   }
 }
 
-Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){
-  //check if there is even any domain elements at all
-  if (!d_rep_set.hasType(tn)) {
-    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-    d_rep_set.d_type_reps[tn].push_back(mbt);
-  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
-    Message() << "empty reps" << std::endl;
-    exit(0);
-  }
-  return d_rep_set.d_type_reps[tn][0];
-}
-
 
 bool FirstOrderModelFmc::isStar(Node n) {
   return n==getStar(n.getType());
@@ -684,3 +697,163 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
     return v==i;
   }
 }
+
+
+FirstOrderModelQInt::FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(qe, c, name) {
+
+}
+
+void FirstOrderModelQInt::processInitialize( bool ispre ) {
+  if( !ispre ){
+    Trace("qint-debug") << "Process initialize" << std::endl;
+    for( std::map<Node, QIntDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) {
+      Node op = it->first;
+      TypeNode tno = op.getType();
+      Trace("qint-debug") << "  Init " << op << " " << tno << std::endl;
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {
+        //make sure a representative of the type exists
+        if( !d_rep_set.hasType( tno[i] ) ){
+          Node e = getSomeDomainElement( tno[i] );
+          Trace("qint-debug") << "  * Initialize type " << tno[i] << ", add ";
+          Trace("qint-debug") << e << " " << e.getType() << std::endl;
+          //d_rep_set.add( e );
+        }
+      }
+    }
+  }
+}
+
+Node FirstOrderModelQInt::getFunctionValue(Node op, const char* argPrefix ) {
+  Trace("qint-debug") << "Get function value for " << op << std::endl;
+  TypeNode type = op.getType();
+  std::vector< Node > vars;
+  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
+    std::stringstream ss;
+    ss << argPrefix << (i+1);
+    Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
+    vars.push_back( b );
+  }
+  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+  Node curr = d_models[op]->getFunctionValue( this, vars );
+  Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+  Trace("qint-debug") << "Return " << fv << std::endl;
+  return fv;
+}
+
+Node FirstOrderModelQInt::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+  Debug("qint-debug") << "get curr uf value " << n << std::endl;
+  return d_models[n]->evaluate( this, args );
+}
+
+void FirstOrderModelQInt::processInitializeModelForTerm(Node n) {
+  Debug("qint-debug") << "process init " << n << " " << n.getKind() << std::endl;
+
+  if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
+    Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
+    if( d_models.find(op)==d_models.end()) {
+      Debug("qint-debug") << "init model for " << op << std::endl;
+      d_models[op] = new QIntDef;
+    }
+  }
+}
+
+Node FirstOrderModelQInt::getUsedRepresentative( Node n ) {
+  if( hasTerm( n ) ){
+    if( n.getType().isBoolean() ){
+      return areEqual(n, d_true) ? d_true : d_false;
+    }else{
+      return getRepresentative( n );
+    }
+  }else{
+    Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl;
+    Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() );
+    return d_rep_set.d_type_reps[n.getType()][0];
+  }
+}
+
+void FirstOrderModelQInt::processInitializeQuantifier( Node q )  {
+  if( d_var_order.find( q )==d_var_order.end() ){
+    d_var_order[q] = new QuantVarOrder( q );
+    d_var_order[q]->debugPrint("qint-var-order");
+    Trace("qint-var-order") << std::endl;
+  }
+}
+unsigned FirstOrderModelQInt::getOrderedNumVars( Node q ) {
+  //return q[0].getNumChildren();
+  return d_var_order[q]->getNumVars();
+}
+
+TypeNode FirstOrderModelQInt::getOrderedVarType( Node q, int i ) {
+  //return q[0][i].getType();
+  return d_var_order[q]->getVar( i ).getType();
+}
+
+int FirstOrderModelQInt::getOrderedVarNumToVarNum( Node q, int i ) {
+  return getVariableId( q, d_var_order[q]->getVar( i ) );
+}
+
+bool FirstOrderModelQInt::isLessThan( Node v1, Node v2 ) {
+  Assert( !v1.isNull() );
+  Assert( !v2.isNull() );
+  if( v1.getType().isSort() ){
+    Assert( getRepId( v1 )!=-1 );
+    Assert( getRepId( v2 )!=-1 );
+    int rid1 = d_rep_id[v1];
+    int rid2 = d_rep_id[v2];
+    return rid1<rid2;
+  }else{
+    return false;
+  }
+}
+
+Node FirstOrderModelQInt::getMin( Node v1, Node v2 ) {
+  return isLessThan( v1, v2 ) ? v1 : v2;
+}
+
+Node FirstOrderModelQInt::getMax( Node v1, Node v2 ) {
+  return isLessThan( v1, v2 ) ? v2 : v1;
+}
+
+Node FirstOrderModelQInt::getMaximum( TypeNode tn ) {
+  return d_max[tn];
+}
+
+Node FirstOrderModelQInt::getNext( TypeNode tn, Node v ) {
+  if( v.isNull() ){
+    return d_min[tn];
+  }else{
+    Assert( getRepId( v )!=-1 );
+    int rid = d_rep_id[v];
+    if( rid==(int)(d_rep_set.d_type_reps[tn].size()-1) ){
+      Assert( false );
+      return Node::null();
+    }else{
+      return d_rep_set.d_type_reps[tn][ rid+1 ];
+    }
+  }
+}
+Node FirstOrderModelQInt::getPrev( TypeNode tn, Node v ) {
+  if( v.isNull() ){
+    Assert( false );
+    return Node::null();
+  }else{
+    Assert( getRepId( v )!=-1 );
+    int rid = d_rep_id[v];
+    if( rid==0 ){
+      return Node::null();
+    }else{
+      return d_rep_set.d_type_reps[tn][ rid-1 ];
+    }
+  }
+}
+
+bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ) {
+  Trace("qint-debug2") << "doMeet " << l1 << "..." << u1 << " with " << l2 << "..." << u2 << std::endl;
+  Assert( !u1.isNull() );
+  Assert( !u2.isNull() );
+  lr = l1.isNull() ? l2 : ( l2.isNull() ? l1 : getMax( l1, l2 ) );
+  ur = getMin( u1, u2 );
+  //return lr==ur || lr.isNull() || isLessThan( lr, ur );
+  return lr.isNull() || isLessThan( lr, ur );
+}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index b5bdff9ee..ab3a1aa52 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -33,16 +33,21 @@ class FirstOrderModelIG;
 namespace fmcheck {
   class FirstOrderModelFmc;
 }
+class FirstOrderModelQInt;
 
 class FirstOrderModel : public TheoryModel
 {
-private:
+protected:
+  /** quant engine */
+  QuantifiersEngine * d_qe;
   /** whether an axiom is asserted */
   context::CDO< bool > d_axiom_asserted;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** is model set */
   context::CDO< bool > d_isModelSet;
+  /** get variable id */
+  std::map< Node, std::map< Node, int > > d_quant_var_id;
   /** get current model value */
   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
@@ -57,20 +62,28 @@ public: //for Theory Quantifiers:
   /** initialize model for term */
   void initializeModelForTerm( Node n );
   virtual void processInitializeModelForTerm( Node n ) = 0;
+  virtual void processInitializeQuantifier( Node q ) {}
 public:
-  FirstOrderModel( context::Context* c, std::string name );
+  FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
   virtual ~FirstOrderModel(){}
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
+  virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
   // initialize the model
   void initialize( bool considerAxioms = true );
-  virtual void processInitialize() = 0;
+  virtual void processInitialize( bool ispre ) = 0;
   /** mark model set */
   void markModelSet() { d_isModelSet = true; }
   /** is model set */
   bool isModelSet() { return d_isModelSet; }
   /** get current model value */
   Node getCurrentModelValue( Node n, bool partial = false );
+  /** get variable id */
+  int getVariableId(Node f, Node n) {
+    return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1;
+  }
+  /** get some domain element */
+  Node getSomeDomainElement(TypeNode tn);
 };/* class FirstOrderModel */
 
 
@@ -93,10 +106,10 @@ private:
   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 //the following functions are for evaluating quantifier bodies
 public:
-  FirstOrderModelIG(context::Context* c, std::string name);
+  FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
   // initialize the model
-  void processInitialize();
+  void processInitialize( bool ispre );
   //for initialize model
   void processInitializeModelForTerm( Node n );
   /** reset evaluation */
@@ -128,8 +141,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 {
   friend class FullModelChecker;
 private:
-  /** quant engine */
-  QuantifiersEngine * d_qe;
   /** models for UF */
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_model_basis_rep;
@@ -143,8 +154,7 @@ public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
-  void processInitialize();
-
+  void processInitialize( bool ispre );
   Node getFunctionValue(Node op, const char* argPrefix );
 
   bool isStar(Node n);
@@ -152,7 +162,6 @@ public:
   Node getStarElement(TypeNode tn);
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
-  Node getSomeDomainElement(TypeNode tn);
   bool isInterval(Node n);
   Node getInterval( Node lb, Node ub );
   bool isInRange( Node v, Node i );
@@ -161,6 +170,50 @@ public:
 }
 
 
+class QIntDef;
+class QuantVarOrder;
+class FirstOrderModelQInt : public FirstOrderModel
+{
+  friend class QIntervalBuilder;
+private:
+  /** uf op to some representation */
+  std::map<Node, QIntDef * > d_models;
+  /** representatives to ids */
+  std::map< Node, int > d_rep_id;
+  std::map< TypeNode, Node > d_min;
+  std::map< TypeNode, Node > d_max;
+  /** quantifiers to information regarding variable ordering */
+  std::map<Node, QuantVarOrder * > d_var_order;
+  /** get current model value */
+  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
+  void processInitializeModelForTerm(Node n);
+public:
+  FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
+  FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
+  void processInitialize( bool ispre );
+  Node getFunctionValue(Node op, const char* argPrefix );
+
+  Node getUsedRepresentative( Node n );
+  int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
+  bool isLessThan( Node v1, Node v2 );
+  Node getMin( Node v1, Node v2 );
+  Node getMax( Node v1, Node v2 );
+  Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
+  Node getMaximum( TypeNode tn );
+  bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
+  bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
+  Node getNext( TypeNode tn, Node v );
+  Node getPrev( TypeNode tn, Node v );
+  bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
+  QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
+
+  void processInitializeQuantifier( Node q ) ;
+  unsigned getOrderedNumVars( Node q );
+  TypeNode getOrderedVarType( Node q, int i );
+  int getOrderedVarNumToVarNum( Node q, int i );
+};
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 2f32ec5e6..174e26a5a 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -588,7 +588,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         std::vector< TypeNode > types;
         for(unsigned i=0; i<f[0].getNumChildren(); i++){
           types.push_back(f[0][i].getType());
-          d_quant_var_id[f][f[0][i]] = i;
         }
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
         Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
@@ -599,7 +598,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         initializeType( fmfmc, f[0][i].getType() );
       }
 
-      if( !options::fmfModelBasedInst() ){
+      if( options::mbqiMode()==MBQI_NONE ){
         //just exhaustive instantiate
         Node c = mkCondDefault( fmfmc, f );
         d_quant_models[f].addEntry( fmfmc, c, d_false );
@@ -958,8 +957,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
   }else{
     TypeNode tn = eq[0].getType();
     if( tn.isSort() ){
-      int j = getVariableId(f, eq[0]);
-      int k = getVariableId(f, eq[1]);
+      int j = fm->getVariableId(f, eq[0]);
+      int k = fm->getVariableId(f, eq[1]);
       if( !fm->d_rep_set.hasType( tn ) ){
         getSomeDomainElement( fm, tn );  //to verify the type is initialized
       }
@@ -977,7 +976,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
 }
 
 void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
-  int j = getVariableId(f, v);
+  int j = fm->getVariableId(f, v);
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     Node val = dc.d_value[i];
     if( val.isNull() ){
@@ -1074,7 +1073,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     Trace("fmc-uf-process") << "Process " << v << std::endl;
     bool bind_var = false;
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
-      int j = getVariableId(f, v);
+      int j = fm->getVariableId(f, v);
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
       if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
         v = cond[j+1];
@@ -1084,7 +1083,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     }
     if (bind_var) {
       Trace("fmc-uf-process") << "bind variable..." << std::endl;
-      int j = getVariableId(f, v);
+      int j = fm->getVariableId(f, v);
       if( fm->isStar(cond[j+1]) ){
         for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
           cond[j+1] = it->first;
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 606392831..db5abb01e 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -92,7 +92,6 @@ protected:
   std::map<Node, Node > d_quant_cond;
   std::map< TypeNode, Node > d_array_cond;
   std::map< Node, Node > d_array_term_cond;
-  std::map<Node, std::map< Node, int > > d_quant_var_id;
   std::map<Node, std::vector< int > > d_star_insts;
   void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
@@ -138,7 +137,6 @@ public:
 
   bool optBuildAtFullModel();
 
-  int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index ea6f2d775..468c78978 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) {
 
 
 bool QModelBuilder::optUseModel() {
-  return options::fmfModelBasedInst() || options::fmfBoundInt();
+  return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt();
 }
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
@@ -124,6 +124,7 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::
 void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
+  Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl;
   if( fullModel ){
     Assert( d_curr_model==fm );
     //update models
@@ -145,7 +146,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
     reset( fm );
     //only construct first order model if optUseModel() is true
     if( optUseModel() ){
-      Trace("model-engine-debug") << "Initializing quantifiers..." << std::endl;
+      Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
       //check if any quantifiers are un-initialized
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
@@ -397,7 +398,6 @@ bool QModelBuilderIG::isTermActive( Node n ){
 //do exhaustive instantiation
 bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
-
     RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
       FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
@@ -456,7 +456,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         d_statistics.d_eval_lits += fmig->d_eval_lits;
         d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
       }
-      Trace("inst-fmf-ei") << "Finished: " << std::endl;
+      Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
       Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
       Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
       if( d_addedLemmas>1000 ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 99f5e8df6..5006a8a61 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/qinterval_builder.h"
 
 using namespace std;
 using namespace CVC4;
@@ -34,11 +36,18 @@ using namespace CVC4::theory::inst;
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ){
 
-  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
+  Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
+  if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){
+    Trace("model-engine-debug") << "...make fmc builder." << std::endl;
     d_builder = new fmcheck::FullModelChecker( c, qe );
-  }else if( options::fmfNewInstGen() ){
+  }else if( options::mbqiMode()==MBQI_INTERVAL ){
+    Trace("model-engine-debug") << "...make interval builder." << std::endl;
+    d_builder = new QIntervalBuilder( c, qe );
+  }else if( options::mbqiMode()==MBQI_INST_GEN ){
+    Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
     d_builder = new QModelBuilderInstGen( c, qe );
   }else{
+    Trace("model-engine-debug") << "...make default model builder." << std::endl;
     d_builder = new QModelBuilderDefault( c, qe );
   }
 
@@ -203,7 +212,7 @@ int ModelEngine::checkModel(){
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
+  int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 0c3c74b5f..fcbba7aee 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -20,7 +20,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/theory_model.h"
-#include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 7da3b150f..10185914e 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -77,5 +77,28 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
+  switch(mode) {
+  case theory::quantifiers::MBQI_DEFAULT:
+    out << "MBQI_DEFAULT";
+    break;
+  case theory::quantifiers::MBQI_NONE:
+    out << "MBQI_NONE";
+    break;
+  case theory::quantifiers::MBQI_INST_GEN:
+    out << "MBQI_INST_GEN";
+    break;
+  case theory::quantifiers::MBQI_FMC:
+    out << "MBQI_FMC";
+    break;
+  case theory::quantifiers::MBQI_INTERVAL:
+    out << "MBQI_INTERVAL";
+    break;
+  default:
+    out << "MbqiMode!UNKNOWN";
+  }
+  return out;
+}
+
 }/* CVC4 namespace */
 
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index edf9c78fe..7c4cb3651 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -55,6 +55,22 @@ typedef enum {
   AXIOM_INST_MODE_PRIORITY,
 } AxiomInstMode;
 
+typedef enum {
+  /** default, mbqi from CADE 24 paper */
+  MBQI_DEFAULT,
+  /** no mbqi */
+  MBQI_NONE,
+  /** implementation that mimics inst-gen */
+  MBQI_INST_GEN,
+  /** mbqi from Section 5.4.2 of AJR thesis */
+  MBQI_FMC,
+  /** mbqi with integer intervals */
+  //MBQI_FMC_INTERVAL,
+  /** mbqi with interval abstraction of uninterpreted sorts */
+  MBQI_INTERVAL,
+} MbqiMode;
+
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 1eb98e7b7..f485b981c 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -95,11 +95,9 @@ option internalReps /--disable-quant-internal-reps bool :default true
 option finiteModelFind --finite-model-find bool :default false
  use finite model finding heuristic for quantifier instantiation
 
-option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
- disable model-based quantifier instantiation for finite model finding
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
+ choose mode for model-based quantifier instantiation
 
-option fmfFullModelCheck --fmf-fmc bool :default false :read-write
- enable full model check for finite model finding
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
 option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
@@ -115,8 +113,6 @@ option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
 option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
-option fmfNewInstGen --fmf-new-inst-gen bool :default false
- use new inst gen technique for answering sat without exhaustive instantiation
 option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
  enable Inst-Gen instantiation techniques for finite model finding (default)
 /disable Inst-Gen instantiation techniques for finite model finding
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 410578af0..a119bcaf6 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -73,6 +73,28 @@ priority \n\
 \n\
 ";
 
+static const std::string mbqiModeHelp = "\
+Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
+\n\
+default \n\
++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper.\n\
+\n\
+none \n\
++ Disable model-based quantifier instantiation.\n\
+\n\
+instgen \n\
++ Use instantiation algorithm that mimics Inst-Gen calculus. \n\
+\n\
+fmc \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\
+  Modulo Theories.\n\
+\n\
+interval \n\
++ Use algorithm that abstracts domain elements as intervals. \n\
+\n\
+";
+
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -135,6 +157,30 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
   }
 }
 
+inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default") {
+    return MBQI_DEFAULT;
+  } else if(optarg ==  "none") {
+    return MBQI_NONE;
+  } else if(optarg ==  "instgen") {
+    return MBQI_INST_GEN;
+  } else if(optarg ==  "fmc") {
+    return MBQI_FMC;
+  } else if(optarg ==  "interval") {
+    return MBQI_INTERVAL;
+  } else if(optarg ==  "help") {
+    puts(mbqiModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --mbqi: `") +
+                          optarg + "'.  Try --mbqi help.");
+  }
+}
+
+inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) {
+
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
new file mode 100755
index 000000000..ce85cecc0
--- /dev/null
+++ b/src/theory/quantifiers/qinterval_builder.cpp
@@ -0,0 +1,1111 @@
+/*********************                                                        */
+/*! \file qinterval_builder.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of qinterval builder
+ **/
+
+
+#include "theory/quantifiers/qinterval_builder.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+//lower bound is exclusive
+//upper bound is inclusive
+
+struct QIntSort
+{
+  FirstOrderModelQInt * m;
+  bool operator() (Node i, Node j) {
+    return m->isLessThan( i, j );
+  }
+};
+
+void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) {
+  for( unsigned i=0; i<m->getOrderedNumVars( q ); i++ ){
+    l.push_back( Node::null() );
+    u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) );
+  }
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u )
+{
+  Trace(c) << "( ";
+  for( unsigned i=0; i<l.size(); i++ ){
+    if( i>0 ) Trace(c) << ", ";
+    //Trace(c) << l[i] << "..." << u[i];
+    int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+    int uindex = m->getRepId( u[i] );
+    Trace(c) << lindex << "..." << uindex;
+  }
+  Trace(c) << " )";
+}
+
+
+int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) {
+  if( n.isNull() ){
+    Assert( exc );
+    return 0;
+  }else{
+    int min = 0;
+    int max = (int)(d_def_order.size()-1);
+    while( min!=max ){
+      int index = (min+max)/2;
+      Assert( index>=0 && index<(int)d_def_order.size() );
+      if( n==d_def_order[index] ){
+        max = index;
+        min = index;
+      }else if( m->isLessThan( n, d_def_order[index] ) ){
+        max = index;
+      }else{
+        min = index+1;
+      }
+    }
+    if( n==d_def_order[min] && exc ){
+      min++;
+    }
+    Assert( min>=0 && min<(int)d_def_order.size() );
+    if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) ||
+        ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){
+      Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl;
+      for( unsigned i=0; i<d_def_order.size(); i++ ){
+        Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];
+        Debug("qint-error") << " " << m->getRepId( d_def_order[i] ) << std::endl;
+      }
+      Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl;
+    }
+
+    Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) );
+    Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) );
+    return min;
+  }
+}
+
+void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+                        Node v, unsigned depth ) {
+  if( depth==0 ){
+    Trace("qint-compose-debug") << "Add entry ";
+    debugPrint( "qint-compose-debug", m, q, l, u );
+    Trace("qint-compose-debug") << " -> " << v << "..." << std::endl;
+  }
+  //Assert( false );
+  if( depth==u.size() ){
+    Assert( d_def_order.empty() );
+    Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) );
+    d_def_order.push_back( v );
+  }else{
+    /*
+    if( !d_def_order.empty() &&
+        ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){
+      int startEvIndex = getEvIndex( m, l[depth], true );
+      int endEvIndex;
+      if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){
+        endEvIndex = getEvIndex( m, u[depth] );
+      }else{
+        endEvIndex = d_def_order.size()-1;
+      }
+      Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl;
+      for( int i=startEvIndex; i<=endEvIndex; i++ ){
+        Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl;
+        d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 );
+      }
+    }
+    if( !d_def_order.empty() &&
+         d_def.find(u[depth])==d_def.end() &&
+         !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+      Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl;
+    }
+    Assert( d_def_order.empty() ||
+            d_def.find(u[depth])!=d_def.end() ||
+            m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) );
+
+    if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+      Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl;
+      d_def_order.push_back( u[depth] );
+      d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 );
+    }
+    */
+    //%%%%%%
+    bool success = true;
+    int nnum = m->getVarOrder( q )->getNextNum( depth );
+    Node pl;
+    Node pu;
+    if( nnum!=-1 ){
+      Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl;
+      //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) );
+      //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) );
+      pl = l[nnum];
+      pu = u[nnum];
+      if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){
+        success = false;
+      }
+    }
+    //%%%%%%
+    if( success ){
+      Node r = u[depth];
+      if( d_def.find( r )!=d_def.end() ){
+        d_def[r].addEntry( m, q, l, u, v, depth+1 );
+      }else{
+        if( !d_def_order.empty() &&
+            !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+          Trace("qint-compose-debug2") << "Bad : depth : " << depth << " ";
+          Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl;
+        }
+        Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) );
+        d_def_order.push_back( r );
+        d_def[r].addEntry( m, q, l, u, v, depth+1 );
+      }
+    }
+    if( nnum!=-1 ){
+      l[nnum] = pl;
+      u[nnum] = pu;
+    }
+  }
+}
+
+Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+                          unsigned depth ) {
+  if( d_def.empty() ){
+    if( d_def_order.size()!=0 ){
+      Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl;
+    }
+    Assert( d_def_order.size()==1 );
+    return d_def_order[0];
+  }else{
+    Assert( !d_def_order.empty() );
+    std::vector< Node > newDefs;
+    Node curr;
+    for( unsigned i=0; i<d_def_order.size(); i++ ){
+      Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );
+      if( i>0 ){
+        if( n==curr && !n.isNull() ){
+          d_def.erase( d_def_order[i-1] );
+        }else{
+          newDefs.push_back( d_def_order[i-1] );
+        }
+      }
+      curr = n;
+    }
+    newDefs.push_back( d_def_order[d_def_order.size()-1] );
+    d_def_order.clear();
+    d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() );
+    return d_def_order.size()==1 ? curr : Node::null();
+  }
+}
+
+Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) {
+  std::vector< Node > l;
+  std::vector< Node > u;
+  if( !q.isNull() ){
+    //init_vec( m, q, l, u );
+  }
+  return simplify_r( m, q, l, u, 0 );
+}
+
+bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+                         unsigned depth ) {
+  if( d_def_order.empty() ){
+    return false;
+  }else if( d_def.empty() ){
+    return true;
+  }else{
+    //get the current maximum
+    Node mx;
+    if( !q.isNull() ){
+      int pnum = m->getVarOrder( q )->getPrevNum( depth );
+      if( pnum!=-1 ){
+        mx = u[pnum];
+      }
+    }
+    if( mx.isNull() ){
+      mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() );
+    }
+    //if not current maximum
+    if( d_def_order[d_def_order.size()-1]!=mx ){
+      return false;
+    }else{
+      Node pu = u[depth];
+      for( unsigned i=0; i<d_def_order.size(); i++ ){
+        u[depth] = d_def_order[i];
+        if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){
+          return false;
+        }
+      }
+      u[depth] = pu;
+      return true;
+    }
+  }
+}
+
+bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {
+  std::vector< Node > l;
+  std::vector< Node > u;
+  if( !q.isNull() ){
+    init_vec( m, q, l, u );
+  }
+  return isTotal_r( m, q, l, u, 0 );
+}
+
+void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q,
+                                    std::vector< Node >& l, std::vector< Node >& u,
+                                    Node n, QIntDef * f,
+                                    std::vector< Node >& args,
+                                    std::map< unsigned, QIntDef >& children,
+                                    std::map< unsigned, Node >& bchildren,
+                                    QIntVarNumIndex& vindex, unsigned depth ) {
+  //check for short circuit
+  if( !f ){
+    if( !args.empty() ){
+      if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) ||
+          ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){
+        addEntry( m, q, l, u, args[args.size()-1] );
+        return;
+      }
+    }
+  }
+
+  for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
+  Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";
+  for( unsigned i=0; i<l.size(); i++ ){
+    if( i>0 ) Trace("qint-compose") << ", ";
+    //Trace("qint-compose") << l[i] << "..." << u[i];
+    int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+    int uindex = m->getRepId( u[i] );
+    Trace( "qint-compose" ) << lindex << "..." << uindex;
+  }
+  Trace("qint-compose") << " )...";
+
+  //finished?
+  if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){
+    if( f ){
+      Assert( f->d_def_order.size()==1 );
+      Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl;
+      addEntry( m, q, l, u, f->d_def_order[0] );
+    }else{
+      Node nn;
+      bool nnSet = false;
+      for( unsigned i=0; i<args.size(); i++ ){
+        if( args[i].isNull() ){
+          nnSet = true;
+          break;
+        }
+      }
+      if( !nnSet ){
+        if( n.getKind()==EQUAL ){
+          nn = NodeManager::currentNM()->mkConst( args[0]==args[1] );
+        }else{
+          //apply the operator to args
+          nn = NodeManager::currentNM()->mkNode( n.getKind(), args );
+          nn = Rewriter::rewrite( nn );
+        }
+      }
+      Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl;
+      addEntry( m, q, l, u, nn );
+      Trace("qint-compose-debug2") << "...added entry." << std::endl;
+    }
+  }else{
+    //if a non-simple child
+    if( children.find( depth )!=children.end() ){
+      //***************************
+      Trace("qint-compose") << "compound child, recurse" << std::endl;
+      std::vector< int > currIndex;
+      std::vector< int > endIndex;
+      std::vector< Node > prevL;
+      std::vector< Node > prevU;
+      std::vector< QIntDef * > visited;
+      do{
+        Assert( currIndex.size()==visited.size() );
+
+        //populate the vectors
+        while( visited.size()<m->getOrderedNumVars( q ) ){
+          unsigned i = visited.size();
+          QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] );
+          visited.push_back( qq );
+          Node qq_mx = qq->getMaximum();
+          Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl;
+          currIndex.push_back( qq->getEvIndex( m, l[i], true ) );
+          Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl;
+          if( m->isLessThan( qq_mx, u[i] ) ){
+            endIndex.push_back( qq->getNumChildren()-1 );
+          }else{
+            endIndex.push_back( qq->getEvIndex( m, u[i] ) );
+          }
+          Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl;
+          prevL.push_back( l[i] );
+          prevU.push_back( u[i] );
+          if( !m->doMeet( prevL[i], prevU[i],
+                          qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){
+            Assert( false );
+          }
+        }
+        for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
+        for( unsigned i=0; i<currIndex.size(); i++ ){
+          Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";
+        }
+        Trace("qint-compose") << std::endl;
+        //consider the current
+        int activeIndex = visited.size()-1;
+        QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( currIndex[activeIndex] );
+        if( f ){
+          int fIndex = f->getEvIndex( m, qa->getValue() );
+          construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 );
+        }else{
+          args.push_back( qa->getValue() );
+          construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+          args.pop_back();
+        }
+
+        //increment the index (if possible)
+        while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){
+          currIndex.pop_back();
+          endIndex.pop_back();
+          l[activeIndex] = prevL[activeIndex];
+          u[activeIndex] = prevU[activeIndex];
+          prevL.pop_back();
+          prevU.pop_back();
+          visited.pop_back();
+          activeIndex--;
+        }
+        if( activeIndex>=0 ){
+          for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
+          Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;
+          currIndex[activeIndex]++;
+          if( !m->doMeet( prevL[activeIndex], prevU[activeIndex],
+                          visited[activeIndex]->getLower( currIndex[activeIndex] ),
+                          visited[activeIndex]->getUpper( currIndex[activeIndex] ),
+                          l[activeIndex], u[activeIndex] ) ){
+            Assert( false );
+          }
+        }
+      }while( !visited.empty() );
+      //***************************
+    }else{
+      Assert( bchildren.find( depth )!=bchildren.end() );
+      Node v = bchildren[depth];
+      if( f ){
+        if( v.getKind()==BOUND_VARIABLE ){
+          int vn = vindex.d_var_num[depth];
+          Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl;
+          //int vn = m->getOrderedVarOccurId( q, n, depth );
+          Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl;
+          Node lprev = l[vn];
+          Node uprev = u[vn];
+          //restrict to last variable in order
+          int pnum = m->getVarOrder( q )->getPrevNum( vn );
+          if( pnum!=-1 ){
+            Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl;
+            l[vn] = l[pnum];
+            u[vn] = u[pnum];
+          }
+          int startIndex = f->getEvIndex( m, l[vn], true );
+          int endIndex = f->getEvIndex( m, u[vn] );
+          Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl;
+          for( int i=startIndex; i<=endIndex; i++ ){
+            if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){
+              construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 );
+            }else{
+              Assert( false );
+            }
+          }
+          l[vn] = lprev;
+          u[vn] = uprev;
+        }else{
+          Trace("qint-compose") << "value, recurse" << std::endl;
+          //simple
+          int ei = f->getEvIndex( m, v );
+          construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 );
+        }
+      }else{
+        Trace("qint-compose") << "value, recurse" << std::endl;
+        args.push_back( v );
+        construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+        args.pop_back();
+      }
+    }
+  }
+}
+
+
+void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) {
+  if( depth==m->getOrderedNumVars( q ) ){
+    Assert( !v.isNull() );
+    d_def_order.push_back( v );
+  }else{
+    TypeNode tn = m->getOrderedVarType( q, depth );
+    //int vnum = m->getVarOrder( q )->getVar( depth )==
+    if( depth==vn ){
+      for( unsigned i=0; i<m->d_rep_set.d_type_reps[tn].size(); i++ ){
+        Node vv = m->d_rep_set.d_type_reps[tn][i];
+        d_def_order.push_back( vv );
+        d_def[vv].construct_enum_r( m, q, vn, depth+1, vv );
+      }
+    }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){
+      d_def_order.push_back( v );
+      d_def[v].construct_enum_r( m, q, vn, depth+1, v );
+    }else{
+      Node mx = m->getMaximum( tn );
+      d_def_order.push_back( mx );
+      d_def[mx].construct_enum_r( m, q, vn, depth+1, v );
+    }
+  }
+}
+
+bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) {
+  TypeNode tn = m->getOrderedVarType( q, vn );
+  if( tn.isSort() ){
+    construct_enum_r( m, q, vn, 0, Node::null() );
+    return true;
+  }else{
+    return false;
+  }
+}
+
+bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+                                 std::map< unsigned, QIntDef >& children,
+                                 std::map< unsigned, Node >& bchildren, int varChCount,
+                                 QIntVarNumIndex& vindex ) {
+ Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted");
+ Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl;
+  std::vector< Node > l;
+  std::vector< Node > u;
+  init_vec( m, q, l, u );
+  if( varChCount==0 || f ){
+    //standard (no variable child) interpreted compose, or uninterpreted compose
+    std::vector< Node > args;
+    construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 );
+  }else{
+    //special cases
+    bool success = false;
+    int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1;
+    if( varChCount>1 ){
+      if( n.getKind()==EQUAL ){
+        //make it an enumeration
+        unsigned vn = vindex.d_var_num[0];
+        if( children[0].construct_enum( m, q, vn ) ){
+          bchildren.erase( 0 );
+          varIndex = 1;
+          success = true;
+        }
+      }
+    }else{
+      success = n.getKind()==EQUAL;
+    }
+    if( success ){
+      int oIndex = varIndex==0 ? 1 : 0;
+      Node v = bchildren[varIndex];
+      unsigned vn = vindex.d_var_num[varIndex];
+      if( children.find( oIndex )==children.end() ){
+        Assert( bchildren.find( oIndex )!=bchildren.end() );
+        Node at = bchildren[oIndex];
+        Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl;
+        Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] );
+        Node above = u[vn];
+        if( !prev.isNull() ){
+          u[vn] = prev;
+          addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+        }
+        l[vn] = prev;
+        u[vn] = at;
+        addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) );
+        if( at!=above ){
+          l[vn] = at;
+          u[vn] = above;
+          addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+        }
+      }else{
+        QIntDef * qid = &children[oIndex];
+        qid->debugPrint("qint-icompose", m, q );
+        Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl;
+
+        TypeNode tn = v.getType();
+        QIntDefIter qdi( m, q, qid );
+        while( !qdi.isFinished() ){
+          std::vector< Node > us;
+          qdi.getUppers( us );
+          std::vector< Node > ls;
+          qdi.getLowers( ls );
+          qdi.debugPrint( "qint-icompose" );
+
+          Node n_below = ls[vn];
+          Node n_prev = m->getPrev( tn, qdi.getValue() );
+          Node n_at = qdi.getValue();
+          Node n_above = us[vn];
+          Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl;
+          if( n.getKind()==EQUAL ){
+            bool atLtAbove = m->isLessThan( n_at, n_above );
+            Node currL = n_below;
+            if( n_at==n_above || atLtAbove ){
+              //add for value (at-1)
+              if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){
+                ls[vn] = currL;
+                us[vn] = n_prev;
+                currL = n_prev;
+                Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl;
+                addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) );
+              }
+              //add for value (at)
+              if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){
+                ls[vn] = currL;
+                us[vn] = n_at;
+                currL = n_at;
+                Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl;
+                addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) );
+              }
+            }
+            ls[vn] = currL;
+            us[vn] = n_above;
+            Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl;
+            addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) );
+          }else{
+            return false;
+          }
+          qdi.increment();
+
+          Trace("qint-icompose-debug") << "Now : " << std::endl;
+          debugPrint("qint-icompose-debug", m, q );
+          Trace("qint-icompose-debug") << std::endl;
+        }
+      }
+
+      Trace("qint-icompose") << "Result : " << std::endl;
+      debugPrint("qint-icompose", m, q );
+      Trace("qint-icompose") << std::endl;
+
+    }else{
+      return false;
+    }
+  }
+  Trace("qint-compose") << "Done i-compose" << std::endl;
+  return true;
+}
+
+
+void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) {
+  d_def.clear();
+  d_def_order.clear();
+  Assert( !fapps.empty() );
+  if( depth==fapps[0].getNumChildren() ){
+    //get representative in model for this term
+    Assert( fapps.size()>=1 );
+    Node r = m->getUsedRepresentative( fapps[0] );
+    d_def_order.push_back( r );
+  }else{
+    std::map< Node, std::vector< Node > > fapp_child;
+    //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
+    for( unsigned i=0; i<fapps.size(); i++ ){
+      Node r = m->getUsedRepresentative( fapps[i][depth] );
+      fapp_child[r].push_back( fapps[i] );
+    }
+    //sort by QIntSort
+    for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
+      d_def_order.push_back( it->first );
+    }
+    QIntSort qis;
+    qis.m = m;
+    std::sort( d_def_order.begin(), d_def_order.end(), qis );
+    //construct children
+    for( unsigned i=0; i<d_def_order.size(); i++ ){
+      Node n = d_def_order[i];
+      if( i==d_def_order.size()-1 ){
+        d_def_order[i] = m->getMaximum( d_def_order[i].getType() );
+      }
+      Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl;
+      d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 );
+    }
+  }
+}
+
+Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) {
+  if( d_def.empty() ){
+    Assert( d_def_order.size()==1 );
+    //must convert to actual domain constant
+    if( d_def_order[0].getType().isSort() ){
+      return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ];
+    }else{
+      return m->getUsedRepresentative( d_def_order[0] );
+    }
+  }else{
+    TypeNode tn = vars[depth].getType();
+    Node curr;
+    int rep_id = m->d_rep_set.getNumRepresentatives( tn );
+    for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){
+      int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1;
+      Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 );
+      if( curr.isNull() ){
+        curr = ccurr;
+      }else{
+        std::vector< Node > c;
+        Assert( curr_rep_id<rep_id );
+        for( int j=curr_rep_id; j<rep_id; j++ ){
+          c.push_back( vars[depth].eqNode( m->d_rep_set.d_type_reps[tn][j] ) );
+        }
+        Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c );
+        curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr );
+      }
+      rep_id = curr_rep_id;
+    }
+    return curr;
+  }
+}
+
+Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) {
+  if( depth==reps.size() ){
+    Assert( d_def_order.size()==1 );
+    return d_def_order[0];
+  }else{
+    if( d_def.find( reps[depth] )!=d_def.end() ){
+      return d_def[reps[depth]].evaluate_r( m, reps, depth+1 );
+    }else{
+      int ei = getEvIndex( m, reps[depth] );
+      return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 );
+    }
+  }
+}
+Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) {
+  if( depth==n.getNumChildren() ){
+    Assert( d_def_order.size()==1 );
+    return d_def_order[0];
+  }else{
+    Node r = m->getUsedRepresentative( n[depth] );
+    if( d_def.find( r )!=d_def.end() ){
+      return d_def[r].evaluate_n_r( m, n, depth+1 );
+    }else{
+      int ei = getEvIndex( m, r );
+      return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 );
+    }
+  }
+}
+
+
+
+QIntDef * QIntDef::getChild( unsigned i ) {
+  Assert( i<d_def_order.size() );
+  Assert( d_def.find( d_def_order[i] )!=d_def.end() );
+  return &d_def[ d_def_order[i] ];
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {
+  /*
+  for( unsigned i=0; i<d_def_order.size(); i++ ){
+    for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+    //Trace(c) << this << " ";
+    Trace(c) << d_def_order[i] << " : " << std::endl;
+    if( d_def.find( d_def_order[i] )!=d_def.end() ){
+      d_def[d_def_order[i]].debugPrint( c, m, t+1 );
+    }
+  }
+  */
+  //if( t==0 ){
+  QIntDefIter qdi( m, q, this );
+  while( !qdi.isFinished() ){
+    qdi.debugPrint( c, t );
+    qdi.increment();
+  }
+  //}
+}
+
+
+QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){
+  resetIndex( qid );
+}
+
+void QIntDefIter::debugPrint( const char * c, int t ) {
+  //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";
+  for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+  std::vector< Node > l;
+  std::vector< Node > u;
+  getLowers( l );
+  getUppers( u );
+  QIntDef::debugPrint( c, d_fm, d_q, l, u );
+  Trace( c ) << " -> " << getValue() << std::endl;
+}
+
+void QIntDefIter::resetIndex( QIntDef * qid ){
+  //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl;
+  if( !qid->d_def.empty() ){
+    //std::cout << "add to visited " <<  qid << std::endl;
+    d_index.push_back( 0 );
+    d_index_visited.push_back( qid );
+    resetIndex( qid->getChild( 0 ) );
+  }
+}
+
+bool QIntDefIter::increment( int index ) {
+  if( !isFinished() ){
+    index = index==-1 ? (int)(d_index.size()-1) : index;
+    while( (int)(d_index.size()-1)>index ){
+      //std::cout << "remove from visit 1 " << std::endl;
+      d_index.pop_back();
+      d_index_visited.pop_back();
+    }
+    while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){
+      //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl;
+      d_index.pop_back();
+      d_index_visited.pop_back();
+      index--;
+    }
+    if( index>=0 ){
+      //std::cout << "increment at index = " << index << std::endl;
+      d_index[index]++;
+      resetIndex( d_index_visited[index]->getChild( d_index[index] ) );
+      return true;
+    }else{
+      d_index.clear();
+      return false;
+    }
+  }else{
+    return false;
+  }
+}
+
+Node QIntDefIter::getLower( int index ) {
+  if( d_index[index]==0 && !d_q.isNull() ){
+    int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index );
+    if( pnum!=-1 ){
+      return getLower( pnum );
+    }
+  }
+  return d_index_visited[index]->getLower( d_index[index] );
+}
+
+Node QIntDefIter::getUpper( int index ) {
+  return d_index_visited[index]->getUpper( d_index[index] );
+}
+
+void QIntDefIter::getLowers( std::vector< Node >& reps ) {
+  for( unsigned i=0; i<getSize(); i++ ){
+    bool added = false;
+    if( d_index[i]==0 && !d_q.isNull() ){
+      int pnum = d_fm->getVarOrder( d_q )->getPrevNum( i );
+      if( pnum!=-1 ){
+        added = true;
+        reps.push_back( reps[pnum] );
+      }
+    }
+    if( !added ){
+      reps.push_back( getLower( i ) );
+    }
+  }
+}
+
+void QIntDefIter::getUppers( std::vector< Node >& reps ) {
+  for( unsigned i=0; i<getSize(); i++ ){
+    reps.push_back( getUpper( i ) );
+  }
+}
+
+Node QIntDefIter::getValue() {
+  return d_index_visited[ d_index_visited.size()-1 ]->getChild( d_index[d_index.size()-1] )->getValue();
+}
+
+
+//------------------------variable ordering----------------------------
+
+QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) {
+  d_var_count = 0;
+  initialize( q[1], 0, d_var_occur );
+}
+
+int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) {
+  if( n.getKind()!=FORALL ){
+    //std::vector< Node > vars;
+    //std::vector< int > args;
+    int procVarOn = n.getKind()==APPLY_UF ? 0 : 1;
+    for( int r=0; r<=procVarOn; r++ ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){
+          int occ_index = -1;
+          for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){
+            if( d_var_to_num[n[i]][j]>=minVarIndex ){
+              occ_index = d_var_to_num[n[i]][j];
+            }
+          }
+          if( occ_index==-1 ){
+            //need to assign new
+            d_num_to_var[d_var_count] = n[i];
+            if( !d_var_to_num[n[i]].empty() ){
+              int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ];
+              d_num_to_prev_num[ d_var_count ] = v;
+              d_num_to_next_num[ v ] = d_var_count;
+            }
+            d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size();
+            d_var_to_num[n[i]].push_back( d_var_count );
+            occ_index = d_var_count;
+            d_var_count++;
+          }
+          vindex.d_var_num[i] = occ_index;
+          minVarIndex = occ_index;
+        }else if( r==0 ){
+          minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] );
+        }
+      }
+    }
+  }
+  return minVarIndex;
+}
+
+bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+                                      std::vector< Node >& inst ) {
+  Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl;
+  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+    Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;
+    Node ll = Node::null();
+    Node uu = m->getMaximum( d_q[0][i].getType() );
+    for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+      Debug("qint-var-order-debug2") << "Go " << j << std::endl;
+      Node cl = ll;
+      Node cu = uu;
+      int index = d_var_to_num[d_q[0][i]][j];
+      Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;
+      Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;
+      if( !m->doMeet( l[index], u[index], cl, cu, ll, uu ) ){
+        Debug("qint-var-order-debug2") << "FAILED" << std::endl;
+        return false;
+      }
+      Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl;
+    }
+    Debug("qint-var-order-debug2") << "Got " << uu << std::endl;
+    inst.push_back( uu );
+  }
+  return true;
+}
+
+void QuantVarOrder::debugPrint( const char * c ) {
+  Trace( c ) << "Variable order for " << d_q << " is : " << std::endl;
+  debugPrint( c, d_q[1], d_var_occur );
+  Trace( c ) << std::endl;
+  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+    Trace( c ) << d_q[0][i] << " : ";
+    for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+      Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";
+    }
+    Trace( c ) << std::endl;
+  }
+}
+
+void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {
+  if( n.getKind()==FORALL ){
+    Trace(c) << "NESTED_QUANT";
+  }else{
+    Trace(c) << n.getKind() << "(";
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( i>0 ) Trace( c ) << ",";
+      Trace( c ) << " ";
+      if( n[i].getKind()==BOUND_VARIABLE ){
+        Trace(c) << "VAR[" << vindex.d_var_num[i] << "]";
+      }else{
+        debugPrint( c, n[i], vindex.d_var_index[i] );
+      }
+      if( i==n.getNumChildren()-1 ) Trace( c ) << " ";
+    }
+    Trace(c) << ")";
+  }
+}
+
+QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ){
+  d_true = NodeManager::currentNM()->mkConst( true );
+}
+
+
+//------------------------model construction----------------------------
+
+void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
+  Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl;
+  FirstOrderModel* f = (FirstOrderModel*)m;
+  FirstOrderModelQInt* fm = f->asFirstOrderModelQInt();
+  if( fullModel ){
+    Trace("qint-model") << "Construct model representation..." << std::endl;
+    //make function values
+    for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      if( it->first.getType().getNumChildren()>1 ){
+        Trace("qint-model") << "Construct for " << it->first << "..." << std::endl;
+        m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
+      }
+    }
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+    //mark that the model has been set
+    fm->markModelSet();
+    //debug the model
+    debugModel( fm );
+  }else{
+    fm->initialize( d_considerAxioms );
+    //process representatives
+    fm->d_rep_id.clear();
+    fm->d_max.clear();
+    fm->d_min.clear();
+    Trace("qint-model") << std::endl << "Making representatives..." << std::endl;
+    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+         it != fm->d_rep_set.d_type_reps.end(); ++it ){
+      if( it->first.isSort() ){
+        if( it->second.empty() ){
+          std::cout << "Empty rep for " << it->first << std::endl;
+          exit(0);
+        }
+        Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Trace("qint-model") << i << " : " << it->second[i] << std::endl;
+          fm->d_rep_id[it->second[i]] = i;
+        }
+        fm->d_min[it->first] = it->second[0];
+        fm->d_max[it->first] = it->second[it->second.size()-1];
+      }else{
+        //TODO: enumerate?
+      }
+    }
+    Trace("qint-model") << std::endl << "Making function definitions..." << std::endl;
+    //construct the models for functions
+    for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      Node f = it->first;
+      Trace("qint-model-debug") << "Building Model for " << f << std::endl;
+      //reset the model
+      //get all (non-redundant) f-applications
+      std::vector< Node > fapps;
+      Trace("qint-model-debug") << "Initial terms: " << std::endl;
+      for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+        Node n = fm->d_uf_terms[f][i];
+        if( !n.getAttribute(NoMatchAttribute()) ){
+          Trace("qint-model-debug") << "  " << n << std::endl;
+          fapps.push_back( n );
+        }
+      }
+      if( fapps.empty() ){
+        //choose arbitrary value
+        Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+        Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+        fapps.push_back( mbt );
+      }
+      //construct the interval model
+      it->second->construct( fm, fapps );
+      Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl;
+      it->second->debugPrint("qint-model-debug", fm, Node::null() );
+
+      it->second->simplify( fm, Node::null() );
+      Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl;
+      it->second->debugPrint("qint-model", fm, Node::null() );
+
+      if( Debug.isOn("qint-model-debug") ){
+        for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+          Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+          Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+          Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
+        }
+      }
+    }
+  }
+}
+
+
+//--------------------model checking---------------------------------------
+
+//do exhaustive instantiation
+bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+  Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+  if (effort==0) {
+
+    FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt();
+    QIntDef qid;
+    doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur );
+    //now process entries
+    Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl;
+    qid.debugPrint( "qint-inst", fmqint, q );
+    Trace("qint-inst") << std::endl;
+    Debug("qint-check-debug2") << "Make iterator..." << std::endl;
+    QIntDefIter qdi( fmqint, q, &qid );
+    while( !qdi.isFinished() ){
+      if( qdi.getValue()!=d_true ){
+        Debug("qint-check-debug2") << "Set up vectors..." << std::endl;
+        std::vector< Node > l;
+        std::vector< Node > u;
+        std::vector< Node > inst;
+        qdi.getLowers( l );
+        qdi.getUppers( u );
+        Debug("qint-check-debug2") << "Get instantiation..." << std::endl;
+        if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
+          Trace("qint-inst") << "** Instantiate with ";
+          //just add the instance
+          InstMatch m;
+          for( unsigned j=0; j<inst.size(); j++) {
+            m.set( d_qe, q, j, inst[j] );
+            Trace("qint-inst") << inst[j] << " ";
+          }
+          Trace("qint-inst") << std::endl;
+          d_triedLemmas++;
+          if( d_qe->addInstantiation( q, m ) ){
+            Trace("qint-inst") << "   ...added instantiation." << std::endl;
+            d_addedLemmas++;
+          }else{
+            Trace("qint-inst") << "   ...duplicate instantiation" << std::endl;
+            //verify that instantiation is witness for current entry
+            if( Debug.isOn("qint-check-debug2") ){
+              Debug("qint-check-debug2") << "Check if : ";
+              std::vector< Node > exp_inst;
+              for( unsigned i=0; i<fmqint->getOrderedNumVars( q ); i++ ){
+                int index = fmqint->getOrderedVarNumToVarNum( q, i );
+                exp_inst.push_back( inst[ index ] );
+                Debug("qint-check-debug2") << inst[index] << " ";
+              }
+              Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl;
+              Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() );
+            }
+          }
+        }else{
+          Trace("qint-inst") << "** Spurious instantiation." << std::endl;
+        }
+      }
+      qdi.increment();
+    }
+  }
+  return true;
+}
+
+bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+                                QIntVarNumIndex& vindex ) {
+  Assert( n.getKind()!=FORALL );
+  std::map< unsigned, QIntDef > children;
+  std::map< unsigned, Node > bchildren;
+  int varChCount = 0;
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    if( n[i].getKind()==FORALL ){
+      bchildren[i] = Node::null();
+    }else if( n[i].getKind() == BOUND_VARIABLE ){
+      varChCount++;
+      bchildren[i] = n[i];
+    }else if( m->hasTerm( n[i] ) ){
+      bchildren[i] = m->getUsedRepresentative( n[i] );
+    }else{
+      if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){
+        bchildren[i] = Node::null();
+      }
+    }
+  }
+  Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
+  if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
+    Node op = n.getKind() == APPLY_UF ? n.getOperator() : n;
+    //uninterpreted compose
+    qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex );
+  }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){
+    Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl;
+    return false;
+  }
+  Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl;
+  qid.debugPrint("qint-check-debug2", m, q);
+  qid.simplify( m, q );
+  Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl;
+  qid.debugPrint("qint-check-debug", m, q);
+  Trace("qint-check-debug") << std::endl;
+  Assert( qid.isTotal( m, q ) );
+  return true;
+}
diff --git a/src/theory/quantifiers/qinterval_builder.h b/src/theory/quantifiers/qinterval_builder.h
new file mode 100755
index 000000000..8f48776cc
--- /dev/null
+++ b/src/theory/quantifiers/qinterval_builder.h
@@ -0,0 +1,155 @@
+/*********************                                                        */
+/*! \file qinterval_builder.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief qinterval model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef QINTERVAL_BUILDER
+#define QINTERVAL_BUILDER
+
+#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class FirstOrderModelQInt;
+
+class QIntVarNumIndex
+{
+public:
+  std::map< int, int > d_var_num;
+  std::map< int, QIntVarNumIndex > d_var_index;
+};
+
+class QIntDef
+{
+private:
+  Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );
+  Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );
+  void construct_compose_r( FirstOrderModelQInt * m, Node q,
+                            std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,
+                            std::vector< Node >& args,
+                            std::map< unsigned, QIntDef >& children,
+                            std::map< unsigned, Node >& bchildren,
+                            QIntVarNumIndex& vindex,
+                            unsigned depth );
+
+  void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );
+  int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );
+  void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+                 Node v, unsigned depth = 0 );
+  Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+                   unsigned depth );
+  bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+                  unsigned depth );
+public:
+  QIntDef(){}
+  std::map< Node, QIntDef > d_def;
+  std::vector< Node > d_def_order;
+
+  void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );
+  bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+                          std::map< unsigned, QIntDef >& children,
+                          std::map< unsigned, Node >& bchildren, int varChCount,
+                          QIntVarNumIndex& vindex );
+  bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );
+
+  Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }
+  Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }
+
+  void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );
+  QIntDef * getChild( unsigned i );
+  Node getValue() { return d_def_order[0]; }
+  Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }
+  Node getUpper( unsigned i ) { return d_def_order[i]; }
+  Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }
+  int getNumChildren() { return d_def_order.size(); }
+  bool isTotal( FirstOrderModelQInt * m, Node q );
+
+  Node simplify( FirstOrderModelQInt * m, Node q );
+  Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );
+
+  static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+  static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+};
+
+class QIntDefIter {
+private:
+  FirstOrderModelQInt * d_fm;
+  Node d_q;
+  void resetIndex( QIntDef * qid );
+public:
+  QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );
+  void debugPrint( const char * c, int t = 0 );
+  std::vector< QIntDef * > d_index_visited;
+  std::vector< int > d_index;
+  bool isFinished() { return d_index.empty(); }
+  bool increment( int index = -1 );
+  unsigned getSize() { return d_index.size(); }
+  Node getLower( int index );
+  Node getUpper( int index );
+  void getLowers( std::vector< Node >& reps );
+  void getUppers( std::vector< Node >& reps );
+  Node getValue();
+};
+
+
+class QuantVarOrder
+{
+private:
+  int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );
+  int d_var_count;
+  Node d_q;
+  void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );
+public:
+  QuantVarOrder( Node q );
+  std::map< int, Node > d_num_to_var;
+  std::map< int, int > d_num_to_prev_num;
+  std::map< int, int > d_num_to_next_num;
+  std::map< Node, std::vector< int > > d_var_to_num;
+  std::map< int, int > d_var_num_index;
+  //std::map< Node, std::map< int, int > > d_var_occur;
+  //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }
+  unsigned getNumVars() { return d_var_count; }
+  Node getVar( int i ) { return d_num_to_var[i]; }
+  int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; }
+  int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; }
+  int getVarNumIndex( int i ) { return d_var_num_index[i]; }
+  bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+                         std::vector< Node >& inst );
+  void debugPrint( const char * c );
+  QIntVarNumIndex d_var_occur;
+};
+
+class QIntervalBuilder : public QModelBuilder
+{
+private:
+  Node d_true;
+  bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+                QIntVarNumIndex& vindex );
+public:
+  QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );
+  //process build model
+  void processBuildModel(TheoryModel* m, bool fullModel);
+  //do exhaustive instantiation
+  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+};
+
+
+}
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e18a4e0dc..6b1368be1 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -146,6 +146,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
              if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
                NoMatchAttribute nma;
                n.setAttribute(nma,true);
+               Debug("term-db-cong") << n << " is redundant." << std::endl;
                congruentCount++;
              }else{
                nonCongruentCount++;
@@ -173,6 +174,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
              if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
                NoMatchAttribute nma;
                en.setAttribute(nma,true);
+               Debug("term-db-cong") << en << " is redundant." << std::endl;
                congruentCount++;
              }else{
                nonCongruentCount++;
@@ -222,10 +224,14 @@ Node TermDb::getModelBasisOpTerm( Node op ){
     TypeNode t = op.getType();
     std::vector< Node > children;
     children.push_back( op );
-    for( size_t i=0; i<t.getNumChildren()-1; i++ ){
+    for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
       children.push_back( getModelBasisTerm( t[i] ) );
     }
-    d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+    if( children.size()==1 ){
+      d_model_basis_op_term[op] = op;
+    }else{
+      d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+    }
   }
   return d_model_basis_op_term[op];
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e9a69bd30..0388a2979 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -49,11 +49,14 @@ d_lemmas_produced_c(u){
   d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
 
+  Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
   //the model object
-  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
+  if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
+  }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
+    d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
   }else{
-    d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
+    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
 
   //add quantifiers modules
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fdd2d0518..43d35ac9d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -254,6 +254,7 @@ protected:
   , d_sharedTerms(satContext)
   , d_out(&out)
   , d_valuation(valuation)
+  , d_proofEnabled(false)
   {
     StatisticsRegistry::registerStat(&d_computeCareGraphTime);
   }
@@ -299,6 +300,12 @@ protected:
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
+  /**
+   * Whether proofs are enabled
+   *
+   */
+  bool d_proofEnabled;
+
 public:
 
   /**
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index cb44b42df..df1d2ebde 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -71,8 +71,8 @@ void EqualityEngine::init() {
   addTermInternal(d_false);
 
   d_trueId = getNodeId(d_true);
-  d_falseId = getNodeId(d_false);  
-} 
+  d_falseId = getNodeId(d_false);
+}
 
 EqualityEngine::~EqualityEngine() throw(AssertionException) {
   free(d_triggerDatabase);
@@ -287,7 +287,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     d_isConstant[result] = t.isConst();
     // If interpreted, set the number of non-interpreted children
     if (isInterpreted) {
-      // How many children are not constants yet 
+      // How many children are not constants yet
       d_subtermsToEvaluate[result] = t.getNumChildren();
       for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
 	if (isConstant(getNodeId(t[i]))) {
@@ -316,11 +316,11 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
       d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags);
       d_newSetTriggers[currentTheory] = tId;
-    } 
+    }
     // Add it to the list for backtracking
     d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
     d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
-    // Mark the the new set as a trigger 
+    // Mark the the new set as a trigger
     d_nodeIndividualTrigger[tId] = newTriggerTermSet();
   }
 
@@ -333,7 +333,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
   propagate();
 
   Assert(hasTerm(t));
-  
+
   Debug("equality") << d_name << "::eq::addTermInternal(" << t << ") => " << result << std::endl;
 }
 
@@ -419,12 +419,12 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
 
     assertEqualityInternal(eq, d_false, reason);
-    propagate();    
-  
+    propagate();
+
     if (d_done) {
       return;
     }
-  
+
     // If both have constant representatives, we don't notify anyone
     EqualityNodeId a = getNodeId(eq[0]);
     EqualityNodeId b = getNodeId(eq[1]);
@@ -432,8 +432,8 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     EqualityNodeId bClassId = getEqualityNode(b).getFind();
     if (d_isConstant[aClassId] && d_isConstant[bClassId]) {
       return;
-    }    
-    
+    }
+
     // If we are adding a disequality, notify of the shared term representatives
     EqualityNodeId eqId = getNodeId(eq);
     TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId];
@@ -443,16 +443,16 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
       // The sets of trigger terms
       TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef);
       TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef);
-      // Go through and notify the shared dis-equalities 
-      Theory::Set aTags = aTriggerTerms.tags;           
-      Theory::Set bTags = bTriggerTerms.tags;           
+      // Go through and notify the shared dis-equalities
+      Theory::Set aTags = aTriggerTerms.tags;
+      Theory::Set bTags = bTriggerTerms.tags;
       TheoryId aTag = Theory::setPop(aTags);
       TheoryId bTag = Theory::setPop(bTags);
       int a_i = 0, b_i = 0;
       while (aTag != THEORY_LAST && bTag != THEORY_LAST) {
         if (aTag < bTag) {
           aTag = Theory::setPop(aTags);
-          ++ a_i;                  
+          ++ a_i;
         } else if (aTag > bTag) {
           bTag = Theory::setPop(bTags);
           ++ b_i;
@@ -499,7 +499,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
 
   Assert(triggersFired.empty());
-  
+
   ++ d_stats.mergesCount;
 
   EqualityNodeId class1Id = class1.getFind();
@@ -539,8 +539,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   TaggedEqualitiesSet class1disequalitiesToNotify;
 
   // Individual tags
-  Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); 
-  Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); 
+  Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags);
+  Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags);
 
   // Only get disequalities if they are not both constant
   if (!class1isConstant || !class2isConstant) {
@@ -590,9 +590,9 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
     Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
     do {
       // Get the current node
-      EqualityNode& currentNode = getEqualityNode(currentId);    
+      EqualityNode& currentNode = getEqualityNode(currentId);
       Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
- 
+
       // Go through the uselist and check for congruences
       UseListNodeId currentUseId = currentNode.getUseList();
       while (currentUseId != null_uselist_id) {
@@ -604,7 +604,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // If it's interpreted and we can interpret
 	if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
-	  // Get the actual term id 
+	  // Get the actual term id
 	  TNode term = d_nodes[funId];
 	  subtermEvaluates(getNodeId(term));
 	}
@@ -622,16 +622,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // There is no representative, so we can add one, we remove this when backtracking
           storeApplicationLookup(funNormalized, funId);
         }
-                  
+
         // Go to the next one in the use list
         currentUseId = useNode.getNext();
       }
-  
+
       // Move to the next node
       currentId = currentNode.getNext();
     } while (currentId != class2Id);
   }
-    
+
   // Now merge the lists
   class1.merge<true>(class2);
 
@@ -660,24 +660,24 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       // Get the triggers
       TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef);
       TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
-      
+
       // Initialize the merged set
       d_newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags);
       d_newSetTriggersSize = 0;
-      
+
       int i1 = 0;
       int i2 = 0;
       Theory::Set tags1 = class1triggers.tags;
       Theory::Set tags2 = class2triggers.tags;
       TheoryId tag1 = Theory::setPop(tags1);
       TheoryId tag2 = Theory::setPop(tags2);
-      
+
       // Comparing the THEORY_LAST is OK because all other theories are
       // smaller, and will therefore be preferred
-      while (tag1 != THEORY_LAST || tag2 != THEORY_LAST) 
+      while (tag1 != THEORY_LAST || tag2 != THEORY_LAST)
       {
         if (tag1 < tag2) {
-          // copy tag1 
+          // copy tag1
           d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
           tag1 = Theory::setPop(tags1);
         } else if (tag1 > tag2) {
@@ -685,7 +685,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           d_newSetTriggers[d_newSetTriggersSize++] = class2triggers.triggers[i2++];
           tag2 = Theory::setPop(tags2);
         } else {
-          // copy tag1 
+          // copy tag1
           EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
           // since they are both tagged notify of merge
           if (d_performNotify) {
@@ -698,17 +698,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           tag1 = Theory::setPop(tags1);
           tag2 = Theory::setPop(tags2);
         }
-      }   
-      
+      }
+
       // Add the new trigger set, if different from previous one
       if (class1triggers.tags != class2triggers.tags) {
         // Add it to the list for backtracking
         d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef));
         d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
-        // Mark the the new set as a trigger 
+        // Mark the the new set as a trigger
         d_nodeIndividualTrigger[class1Id] = newTriggerTermSet();
-      }  
-    }	
+      }
+    }
   }
 
   // Everything fine
@@ -792,14 +792,14 @@ void EqualityEngine::backtrack() {
     }
     d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
   }
-  
+
   if (d_equalityTriggers.size() > d_equalityTriggersCount) {
     // Unlink the triggers from the lists
     for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
       const Trigger& trigger = d_equalityTriggers[i];
       d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
     }
-    // Get rid of the triggers 
+    // Get rid of the triggers
     d_equalityTriggers.resize(d_equalityTriggersCount);
     d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
   }
@@ -859,7 +859,7 @@ void EqualityEngine::backtrack() {
     d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
     d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
   }
-  
+
 }
 
 void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
@@ -892,7 +892,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
   return out.str();
 }
 
-void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities) const {
+void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
   Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl;
 
   // The terms must be there already
@@ -904,7 +904,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
 
   if (polarity) {
     // Get the explanation
-    getExplanation(t1Id, t2Id, equalities);
+    getExplanation(t1Id, t2Id, equalities, eqp);
   } else {
     // Get the reason for this disequality
     EqualityPair pair(t1Id, t2Id);
@@ -912,20 +912,20 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
-      getExplanation(toExplain.first, toExplain.second, equalities);
+      getExplanation(toExplain.first, toExplain.second, equalities, eqp);
     }
   }
 }
 
-void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions) const {
+void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const {
   Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl;
   // Must have the term
   Assert(hasTerm(p));
   // Get the explanation
-  getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions);
+  getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp);
 }
 
-void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
+void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const {
 
   Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
 
@@ -933,17 +933,23 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 #ifdef CVC4_ASSERTIONS
   bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind()
                   || (d_done && isConstant(t1Id) && isConstant(t2Id));
-  
+
   if (!canExplain) {
     Warning() << "Can't explain equality:" << std::endl;
     Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
-    Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;    
+    Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;
   }
   Assert(canExplain);
 #endif
 
   // If the nodes are the same, we're done
-  if (t1Id == t2Id) return;
+  if (t1Id == t2Id){
+    if( eqp ) {
+      eqp->d_node = d_nodes[t1Id];
+    }
+    return;
+  }
+
 
   if (Debug.isOn("equality::internal")) {
     debugPrintGraph();
@@ -986,6 +992,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
           Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
 
+          std::vector< EqProof * > eqp_trans;
+
           // Reconstruct the path
           do {
             // The current node
@@ -995,6 +1003,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
 
+            EqProof * eqpc = NULL;
+            //make child proof if a proof is being constructed
+            if( eqp ){
+              eqpc = new EqProof;
+              eqpc->d_id = reasonType;
+            }
             // Add the actual equality to the vector
             switch (reasonType) {
             case MERGED_THROUGH_CONGRUENCE: {
@@ -1003,32 +1017,45 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               const FunctionApplication& f1 = d_applications[currentNode].original;
               const FunctionApplication& f2 = d_applications[edgeNode].original;
               Debug("equality") << push;
-              getExplanation(f1.a, f2.a, equalities);
-              getExplanation(f1.b, f2.b, equalities);
+              EqProof * eqpc1 = eqpc ? new EqProof : NULL;
+              getExplanation(f1.a, f2.a, equalities, eqpc1);
+              EqProof * eqpc2 = eqpc ? new EqProof : NULL;
+              getExplanation(f1.b, f2.b, equalities, eqpc2);
+              if( eqpc ){
+                eqpc->d_children.push_back( eqpc1 );
+                eqpc->d_children.push_back( eqpc2 );
+              }
               Debug("equality") << pop;
               break;
-            } 
+            }
             case MERGED_THROUGH_EQUALITY:
               // Construct the equality
               Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
+              if( eqpc ){
+                eqpc->d_node = d_equalityEdges[currentEdge].getReason();
+              }
               equalities.push_back(d_equalityEdges[currentEdge].getReason());
               break;
             case MERGED_THROUGH_REFLEXIVITY: {
-              // x1 == x1 
+              // x1 == x1
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
               EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
               const FunctionApplication& eq = d_applications[eqId].original;
               Assert(eq.isEquality(), "Must be an equality");
-              
+
               // Explain why a = b constant
               Debug("equality") << push;
-              getExplanation(eq.a, eq.b, equalities);
+              EqProof * eqpc1 = eqpc ? new EqProof : NULL;
+              getExplanation(eq.a, eq.b, equalities, eqpc1);
+              if( eqpc ){
+                eqpc->d_children.push_back( eqpc1 );
+              }
               Debug("equality") << pop;
-              
-              break;              
+
+              break;
             }
             case MERGED_THROUGH_CONSTANTS: {
-              // f(c1, ..., cn) = c semantically, we can just ignore it 
+              // f(c1, ..., cn) = c semantically, we can just ignore it
               Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
               Debug("equality") << push;
 
@@ -1042,7 +1069,11 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
                 EqualityNodeId childId = getNodeId(interpreted[i]);
                 Assert(isConstant(childId));
-                getExplanation(childId, getEqualityNode(childId).getFind(), equalities);
+                EqProof * eqpcc = eqpc ? new EqProof : NULL;
+                getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
+                if( eqpc ) {
+                  eqpc->d_children.push_back( eqpcc );
+                }
               }
 
               Debug("equality") << pop;
@@ -1051,14 +1082,21 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             }
             default:
               Unreachable();
-            }  
-            
+            }
+
             // Go to the previous
             currentEdge = bfsQueue[currentIndex].edgeId;
             currentIndex = bfsQueue[currentIndex].previousIndex;
-          
+
+            eqp_trans.push_back( eqpc );
+
           } while (currentEdge != null_id);
 
+          if( eqp ){
+            eqp->d_id = MERGED_THROUGH_TRANS;
+            eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+          }
+
           // Done
           return;
         }
@@ -1220,7 +1258,7 @@ void EqualityEngine::processEvaluationQueue() {
     // Get the node
     EqualityNodeId id = d_evaluationQueue.front();
     d_evaluationQueue.pop();
-    
+
     // Replace the children with their representatives (must be constants)
     Node nodeEvaluated = evaluateTerm(d_nodes[id]);
     Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl;
@@ -1240,11 +1278,11 @@ void EqualityEngine::propagate() {
   if (d_inPropagate) {
     // We're already in propagate, go back
     return;
-  } 
-  
+  }
+
   // Make sure we don't get in again
   ScopedBool inPropagate(d_inPropagate, true);
-  
+
   Debug("equality") << d_name << "::eq::propagate()" << std::endl;
 
   while (!d_propagationQueue.empty() || !d_evaluationQueue.empty()) {
@@ -1255,13 +1293,13 @@ void EqualityEngine::propagate() {
       while (!d_evaluationQueue.empty()) d_evaluationQueue.pop();
       continue;
     }
-    
+
     // Process any evaluation requests
     if (!d_evaluationQueue.empty()) {
       processEvaluationQueue();
       continue;
     }
-    
+
     // The current merge candidate
     const MergeCandidate current = d_propagationQueue.front();
     d_propagationQueue.pop_front();
@@ -1288,7 +1326,7 @@ void EqualityEngine::propagate() {
     // Add the actual equality to the equality graph
     addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
 
-    // If constants are being merged we're done 
+    // If constants are being merged we're done
     if (d_isConstant[t1classId] && d_isConstant[t2classId]) {
       // When merging constants we are inconsistent, hence done
       d_done = true;
@@ -1462,7 +1500,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       return true;
     }
   }
- 
+
   // Check the other equality itself if it exists
   eq = t2.eqNode(t1);
   if (hasTerm(eq)) {
@@ -1474,7 +1512,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       return true;
     }
   }
-  
+
   // Create the equality
   FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
   ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized);
@@ -1492,7 +1530,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       return true;
     }
   }
-  
+
   // Check the symmetric disequality
   std::swap(eqNormalized.a, eqNormalized.b);
   find = d_applicationLookup.find(eqNormalized);
@@ -1510,7 +1548,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       return true;
     }
   }
-    
+
   // Couldn't deduce dis-equalityReturn whether the terms are disequal
   return false;
 }
@@ -1568,19 +1606,19 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
       // Initialize the new set for copy/insert
       d_newSetTags = Theory::setInsert(tag, triggerSet.tags);
       d_newSetTriggersSize = 0;
-      // Copy into to new one, and insert the new tag/id      
+      // Copy into to new one, and insert the new tag/id
       unsigned i = 0;
       Theory::Set tags = d_newSetTags;
-      TheoryId current; 
+      TheoryId current;
       while ((current = Theory::setPop(tags)) != THEORY_LAST) {
         // Remove from the tags
         tags = Theory::setRemove(current, tags);
         // Insert the id into the triggers
-        d_newSetTriggers[d_newSetTriggersSize++] = 
+        d_newSetTriggers[d_newSetTriggersSize++] =
           current == tag ? eqNodeId : triggerSet.triggers[i++];
       }
     } else {
-      // Setup a singleton 
+      // Setup a singleton
       d_newSetTags = Theory::setInsert(tag);
       d_newSetTriggers[0] = eqNodeId;
       d_newSetTriggersSize = 1;
@@ -1589,7 +1627,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
     // Add it to the list for backtracking
     d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef));
     d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
-    // Mark the the new set as a trigger 
+    // Mark the the new set as a trigger
     d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet();
 
     // Propagate trigger term disequalities we remembered
@@ -1843,7 +1881,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
 }
 
 bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) {
-  
+
   // No tags, no food
   if (!tags) {
     return !d_done;
@@ -1852,14 +1890,14 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
   Assert(triggerSetRef != null_set_id);
 
   // This is the class trigger set
-  const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); 
+  const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
   // Go through the disequalities and notify
   TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin();
   TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end();
   for (; !d_done && it != it_end; ++ it) {
     // The information about the equality that is asserted to false
     const TaggedEquality& disequalityInfo = *it;
-    const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); 
+    const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef);
     Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags);
     Assert(commonTags);
     // This is the actual function
@@ -1897,7 +1935,7 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
       }
     }
   }
-  
+
   return !d_done;
 }
 
@@ -2005,6 +2043,25 @@ bool EqClassIterator::isFinished() const {
 }
 
 
+void EqProof::debug_print( const char * c, unsigned tb ){
+  for( unsigned i=0; i<tb; i++ ) { Debug( c ) << "  "; }
+  Debug( c ) << d_id << "(";
+  if( !d_children.empty() || !d_node.isNull() ){
+    if( !d_node.isNull() ){
+      Debug( c ) << std::endl;
+      for( unsigned i=0; i<tb+1; i++ ) { Debug( c ) << "  "; }
+      Debug( c ) << d_node;
+    }
+    for( unsigned i=0; i<d_children.size(); i++ ){
+      if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
+      std::cout << std::endl;
+      d_children[i]->debug_print( c, tb+1 );
+    }
+  }
+  Debug( c ) << ")";
+}
+
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index ab106bc8d..f8e361081 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -39,6 +39,8 @@ namespace CVC4 {
 namespace theory {
 namespace eq {
 
+
+class EqProof;
 class EqClassesIterator;
 class EqClassIterator;
 
@@ -421,35 +423,35 @@ private:
   /**
    * Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted
    * application to a constant, we can decrease this value. If we hit 0, we can evaluate the term.
-   * 
+   *
    */
   std::vector<unsigned> d_subtermsToEvaluate;
-  
-  /** 
+
+  /**
    * For nodes that we need to postpone evaluation.
    */
   std::queue<EqualityNodeId> d_evaluationQueue;
-  
+
   /**
    * Evaluate all terms in the evaluation queue.
    */
   void processEvaluationQueue();
-  
+
   /** Vector of nodes that evaluate. */
   std::vector<EqualityNodeId> d_subtermEvaluates;
 
   /** Size of the nodes that evaluate vector. */
   context::CDO<unsigned> d_subtermEvaluatesSize;
-  
+
   /** Set the node evaluate flag */
   void subtermEvaluates(EqualityNodeId id);
 
   /**
-   * Returns the evaluation of the term when all (direct) children are replaced with 
+   * Returns the evaluation of the term when all (direct) children are replaced with
    * the constant representatives.
    */
   Node evaluateTerm(TNode node);
-  
+
   /**
    * Returns true if it's a constant
    */
@@ -487,7 +489,7 @@ private:
 
   /** Enqueue to the propagation queue */
   void enqueue(const MergeCandidate& candidate, bool back = true);
-  
+
   /** Do the propagation */
   void propagate();
 
@@ -499,7 +501,7 @@ private:
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
    * else.
    */
-  void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
+  void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const;
 
   /**
    * Print the equality graph.
@@ -752,7 +754,7 @@ public:
   void assertPredicate(TNode p, bool polarity, TNode reason);
 
   /**
-   * Adds predicate p and q and makes them equal. 
+   * Adds predicate p and q and makes them equal.
    */
   void mergePredicates(TNode p, TNode q, TNode reason);
 
@@ -782,14 +784,14 @@ public:
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */
-  void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const;
+  void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
 
   /**
    * Get an explanation of the predicate being true or false.
    * Returns the reasons (added when asserting) that imply imply it
    * in the assertions vector.
    */
-  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions) const;
+  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
 
   /**
    * Add term to the set of trigger terms with a corresponding tag. The notify class will get
@@ -890,6 +892,16 @@ public:
   bool isFinished() const;
 };/* class EqClassIterator */
 
+class EqProof
+{
+public:
+  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
+  MergeReasonType d_id;
+  Node d_node;
+  std::vector< EqProof * > d_children;
+  void debug_print( const char * c, unsigned tb = 0 );
+};
+
 } // Namespace eq
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index a36291974..435a1ece5 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -54,7 +54,7 @@ static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);
 
 /**
  * A reason for a merge. Either an equality x = y, a merge of two
- * function applications f(x1, x2), f(y1, y2) due to congruence, 
+ * function applications f(x1, x2), f(y1, y2) due to congruence,
  * or a merge of an equality to false due to both sides being
  * (different) constants.
  */
@@ -67,6 +67,9 @@ enum MergeReasonType {
   MERGED_THROUGH_REFLEXIVITY,
   /** Equality was merged to false, due to both sides of equality being a constant */
   MERGED_THROUGH_CONSTANTS,
+
+  /** (for proofs only) Equality was merged due to transitivity */
+  MERGED_THROUGH_TRANS,
 };
 
 inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
@@ -83,6 +86,10 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_CONSTANTS:
     out << "constants disequal";
     break;
+  // (for proofs only)
+  case MERGED_THROUGH_TRANS:
+    out << "transitivity";
+    break;
   default:
     Unreachable();
   }
@@ -98,7 +105,7 @@ struct MergeCandidate {
   MergeReasonType type;
   TNode reason;
   MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
-  : t1Id(x), t2Id(y), type(type), reason(reason) 
+  : t1Id(x), t2Id(y), type(type), reason(reason)
   {}
 };
 
@@ -112,9 +119,9 @@ struct DisequalityReasonRef {
   : mergesStart(mergesStart), mergesEnd(mergesEnd) {}
 };
 
-/** 
+/**
  * We maintain uselist where a node appears in, and this is the node
- * of such a list. 
+ * of such a list.
  */
 class UseListNode {
 
@@ -150,12 +157,12 @@ public:
 };
 
 /**
- * Main class for representing nodes in the equivalence class. The 
+ * Main class for representing nodes in the equivalence class. The
  * nodes are a circular list, with the representative carrying the
  * size. Each individual node carries with itself the uselist of
- * function applications it appears in and the list of asserted 
+ * function applications it appears in and the list of asserted
  * disequalities it belongs to. In order to get these lists one must
- * traverse the entire class and pick up all the individual lists. 
+ * traverse the entire class and pick up all the individual lists.
  */
 class EqualityNode {
 
@@ -180,7 +187,7 @@ public:
    */
   EqualityNode(EqualityNodeId nodeId = null_id)
   : d_size(1)
-  , d_findId(nodeId) 
+  , d_findId(nodeId)
   , d_nextId(nodeId)
   , d_useList(null_uselist_id)
   {}
@@ -232,7 +239,7 @@ public:
 
   /**
    * Note that this node is used in a function application funId, or
-   * a negatively asserted equality (dis-equality) with funId. 
+   * a negatively asserted equality (dis-equality) with funId.
    */
   template<typename memory_class>
   void usedIn(EqualityNodeId funId, memory_class& memory) {
@@ -275,8 +282,8 @@ enum FunctionApplicationType {
 
 /**
  * Represents the function APPLY a b. If isEquality is true then it
- * represents the predicate (a = b). Note that since one can not 
- * construct the equality over function terms, the equality and hash 
+ * represents the predicate (a = b). Note that since one can not
+ * construct the equality over function terms, the equality and hash
  * function below are still well defined.
  */
 struct FunctionApplication {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1045c5a24..fd46ed7f4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -178,10 +178,16 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
+  eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp);
+  }
+  //for now, just print debug
+  //TODO : send the proof outwards : d_out->conflict( lem, eqp );
+  if( eqp ){
+    eqp->debug_print("uf-pf");
   }
 }
 
@@ -462,6 +468,7 @@ void TheoryUF::computeCareGraph() {
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {
+  //TODO: create EqProof at this level if d_proofEnabled = true
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b));
   } else {
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 409b41e3f..3b59c1c58 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -346,23 +346,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground
   d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;
   if( optUsePartialDefaults() ){
     if( !ground ){
-      if (!options::fmfFullModelCheck()) {
-        int defSize = (int)d_defaults.size();
-        for( int i=0; i<defSize; i++ ){
-          //for soundness, to allow variable order-independent function interpretations,
-          //  we must ensure that the intersection of all default terms
-          //  is also defined.
-          //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
-          //  then we must define f( b, a ).
-          bool isGround;
-          Node ni = getIntersection( m, n, d_defaults[i], isGround );
-          if( !ni.isNull() ){
-            //if the intersection exists, and is not already defined
-            if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
-                d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
-              //use the current value
-              setValue( m, ni, v, isGround, false );
-            }
+      int defSize = (int)d_defaults.size();
+      for( int i=0; i<defSize; i++ ){
+        //for soundness, to allow variable order-independent function interpretations,
+        //  we must ensure that the intersection of all default terms
+        //  is also defined.
+        //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
+        //  then we must define f( b, a ).
+        bool isGround;
+        Node ni = getIntersection( m, n, d_defaults[i], isGround );
+        if( !ni.isNull() ){
+          //if the intersection exists, and is not already defined
+          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+            //use the current value
+            setValue( m, ni, v, isGround, false );
           }
         }
       }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 052b2f568..a4cefe269 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1338,6 +1338,21 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
           d_sym_break_terms[n.getType()][sort_id].push_back( n );
           d_sym_break_index[n] = use_cardinality;
           Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl;
+          if( d_sym_break_terms[n.getType()][sort_id].size()>1 ){
+            //enforce canonicity
+            for( int i=2; i<use_cardinality; i++ ){
+              //can only be assigned to domain constant d if someone has been assigned domain constant d-1
+              Node eq = n.eqNode( getTotalityLemmaTerm( cardinality, i ) );
+              std::vector< Node > eqs;
+              for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
+                eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
+              }
+              Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+              Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
+              Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
+              d_thss->getOutputChannel().lemma( lem );
+            }
+          }
         }
       }
 
@@ -1499,6 +1514,7 @@ void StrongSolverTheoryUF::newEqClass( Node n ){
     if( options::ufssSymBreak() ){
       d_sym_break->newEqClass( n );
     }
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
   }
 }
 
@@ -1508,6 +1524,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
   if( c ){
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
     c->merge( a, b );
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
   }else{
     if( options::ufssDiseqPropagation() ){
       d_deq_prop->merge(a, b);
@@ -1523,6 +1540,7 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
     //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
     //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
     c->assertDisequal( a, b, reason );
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl;
   }else{
     if( options::ufssDiseqPropagation() ){
       d_deq_prop->assertDisequal(a, b, reason);