From 65c54b87d09495c711f9a0b140c875f814b9ec07 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 19 Feb 2014 13:57:27 -0800
Subject: [PATCH] duality fix

---
 src/duality/duality.h          | 6 +++---
 src/duality/duality_rpfp.cpp   | 8 +++++++-
 src/duality/duality_solver.cpp | 4 ++--
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index aacc04f24..e1d058f10 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1242,17 +1242,17 @@ namespace Duality {
 
       void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
 
-      edge_solver &SolverForEdge(Edge *edge, bool models);
+      edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms);
 
   public:
       struct scoped_solver_for_edge {
 	solver *orig_slvr;
 	RPFP_caching *rpfp;
 	edge_solver *es;
-	scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
+	scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
 	  rpfp = _rpfp;
 	  orig_slvr = rpfp->ls->slvr;
-	  es = &(rpfp->SolverForEdge(edge,models)); 
+	  es = &(rpfp->SolverForEdge(edge,models,axioms)); 
 	  rpfp->ls->slvr = es->slvr.get();
 	  rpfp->AssumptionLits.swap(es->AssumptionLits);
 	}
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 173959567..6b9f3ba00 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -2895,12 +2895,18 @@ namespace Duality {
     timer_stop("Generalize");
   }
 
-  RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models){
+  RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){
     edge_solver &es = edge_solvers[edge];
     uptr<solver> &p = es.slvr;
     if(!p.get()){
       scoped_no_proof no_proofs_please(ctx.m()); // no proofs
       p.set(new solver(ctx,true,models)); // no models
+      if(axioms){
+	RPFP::LogicSolver *ls = edge->owner->ls;
+	const std::vector<expr> &axs = ls->get_axioms();
+	for(unsigned i = 0; i < axs.size(); i++)
+	  p.get()->add(axs[i]);
+      }
     }
     return es;
   }
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index e3a294550..277789ce9 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -1247,7 +1247,7 @@ namespace Duality {
 	slvr.pop(1);
 	delete checker;
 #else
-	RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
+	RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
 	gen_cands_rpfp->Push();
 	Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
 	if(gen_cands_rpfp->Check(root) != unsat){
@@ -2004,7 +2004,7 @@ namespace Duality {
 	  }
 	  else {
 	    was_sat = true;
-	    tree->Push();
+	    tree->Push();

 	    std::vector<Node *> &expansions = stack.back().expansions;
 #ifndef NO_DECISIONS
 	    for(unsigned i = 0; i < expansions.size(); i++){