diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 80af7eeb0..ca7277d07 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -985,6 +985,9 @@ namespace datalog {
             flush_add_rules();
             break;
         case DUALITY_ENGINE:
+	    // this lets us use duality with SAS 2013 abstraction
+	    if(quantify_arrays())
+	      flush_add_rules();
 	    break;
         default:
             UNREACHABLE();
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index c7fa0a08f..7666b39cf 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -37,6 +37,7 @@ Revision History:
 #include "fixedpoint_params.hpp"
 #include "used_vars.h"
 #include "func_decl_dependencies.h"
+#include "dl_transforms.h"
 
 // template class symbol_table<family_id>;
 
@@ -158,22 +159,34 @@ lbool dl_interface::query(::expr * query) {
   vector<unsigned> bounds;
   // m_ctx.get_rules_as_formulas(rules, names);
 
+
+  // If using SAS 2013 abstractiion, we need to perform some transforms
   expr_ref query_ref(m_ctx.get_manager());
-  if(****){
-    m_ctx.flush_add_rules();
+  if(m_ctx.quantify_arrays()){
     datalog::rule_manager& rm = m_ctx.get_rule_manager();
     rm.mk_query(query, m_ctx.get_rules());
     apply_default_transformation(m_ctx);
-    rule_set &rs = m_ctx.get_rules();
+    datalog::rule_set &rs = m_ctx.get_rules();
     if(m_ctx.get_rules().get_output_predicates().empty())
-      query_ref = m_ctx.get_manager().mk_true();
+        query_ref = m_ctx.get_manager().mk_false();
     else {
-          query_pred = m_ctx.get_rules().get_output_predicate();
-	  func_decl_ref query_pred(m_ctx.get_manager());
-	  query_pred = m_ctx.get_rules().get_output_predicate();
-	  ptr_vector<sort> sorts;
-	  unsi
-
+        func_decl_ref query_pred(m_ctx.get_manager());
+	query_pred = m_ctx.get_rules().get_output_predicate();
+	ptr_vector<sort> sorts;
+	unsigned nargs = query_pred.get()->get_arity();
+	expr_ref_vector vars(m_ctx.get_manager());
+	for(unsigned i = 0; i < nargs; i++){
+	  ::sort *s = query_pred.get()->get_domain(i);
+	  vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
+	}
+	query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
+	query = query_ref.get();
+    }
+    unsigned nrules = rs.get_num_rules();
+    for(unsigned i = 0; i < nrules; i++){
+      expr_ref f(m_ctx.get_manager());
+      rs.get_rule(i)->to_formula(f);
+      rules.push_back(f);
     }
   }
   else