diff --git a/bench/run-bench.sh b/bench/run-bench.sh
new file mode 100755
index 000000000..6c8e41157
--- /dev/null
+++ b/bench/run-bench.sh
@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+
diff --git a/bench_adt/heap_insert.smt2 b/bench_adt/heap_insert_eq.smt2
similarity index 100%
rename from bench_adt/heap_insert.smt2
rename to bench_adt/heap_insert_eq.smt2
diff --git a/bench_adt/run-bench.sh b/bench_adt/run-bench.sh
new file mode 100755
index 000000000..a40b591df
--- /dev/null
+++ b/bench_adt/run-bench.sh
@@ -0,0 +1,77 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+opensmt=../opensmt
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    opensmt=$1
+fi
+
+# run the interpolating version of OpenSMT
+opensmt=${opensmt}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${opensmt} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null 
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+    sh -c "ulimit -St 60; ${opensmt} $picky $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for picky benchmark $file";
+        err=true;
+    fi
+
+    sh -c "ulimit -St 60; ${opensmt} $lookahead $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for lookahead benchmark $file";
+        err=true;
+    fi
+
+    #diff -q ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    #if [ $? != 0 ]; then
+    #    echo "stdout differs for benchmark $file";
+    #    outmod=true;
+    #    diff ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    #fi
+    #diff -q ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    #if [ $? != 0 ]; then
+    #    echo "stderr differs for benchmark $file";
+    #    errmod=true;
+    #    diff ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    #fi
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+
diff --git a/bench_horn_adt/ADTIND/list_len_acc.smt2 b/bench_horn_adt/ADTIND/list_len_acc.smt2
new file mode 100644
index 000000000..c725a6a1e
--- /dev/null
+++ b/bench_horn_adt/ADTIND/list_len_acc.smt2
@@ -0,0 +1,10 @@
+(set-logic HORN)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-fun length (Lst Int) Bool)
+(declare-fun ff () Bool)
+(assert (length nil 0))
+
+(assert (forall ((x Int) (xs Lst) (ys Lst) (l Int))
+       (=> (and (= xs (cons x ys)) (length ys l) (not (length (tail xs) l))) ff)))
+(assert (not ff))
+(check-sat)
\ No newline at end of file
diff --git a/bench_horn_adt/ADTIND/list_value_check_acc.smt2 b/bench_horn_adt/ADTIND/list_value_check_acc.smt2
new file mode 100644
index 000000000..0cd73991e
--- /dev/null
+++ b/bench_horn_adt/ADTIND/list_value_check_acc.smt2
@@ -0,0 +1,11 @@
+;There is some weird error rn
+(set-logic HORN)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-fun length (Lst Int) Bool)
+(declare-fun ff () Bool)
+
+;(assert (length nil 0))
+(assert (forall ((x1 Int) (x2 Int) (xs Lst) (ys Lst) (zs Lst) (l Int))
+       (=> (and (= xs (cons x1 ys)) (= ys (cons x2 zs)) (not (= (head (tail xs)) x2))) ff)))
+(assert (not ff))
+(check-sat)
\ No newline at end of file
diff --git a/bench_horn_adt/run-bench.sh b/bench_horn_adt/run-bench.sh
new file mode 100755
index 000000000..6c8e41157
--- /dev/null
+++ b/bench_horn_adt/run-bench.sh
@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+
diff --git a/bench_sim/run-bench.sh b/bench_sim/run-bench.sh
new file mode 100755
index 000000000..6c8e41157
--- /dev/null
+++ b/bench_sim/run-bench.sh
@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+
diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp
index fec9a2a92..649cb65d7 100644
--- a/include/adt/CHCSolver.hpp
+++ b/include/adt/CHCSolver.hpp
@@ -18,6 +18,7 @@ namespace ufo
     // Keep the current return values
     std::map<Expr,int> values_inds;
     ExprVector &constructors;
+    ExprVector &accessors;
     ExprVector &assumptions;
 
     ExprSet &decls;
@@ -35,8 +36,8 @@ namespace ufo
     map<Expr, Expr> interpretations;
 
   public:
-    CHCSolver(ExprVector& _constructors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector<HornRuleExt> &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) :
-      constructors(_constructors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {}
+    CHCSolver(ExprVector& _constructors, ExprVector& _accessors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector<HornRuleExt> &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) :
+      constructors(_constructors), accessors(_accessors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {}
 
     Expr createNewApp(HornRuleExt chc, int i, int ind) {
       ExprVector types;
@@ -92,6 +93,17 @@ namespace ufo
           }
         }
       }
+      // TODO: HERE I NEED TO CHECK IF WHAT I HAVE ON THE RIGHT IS AN ACCESSOR
+      if ((elem->right()->arity() == 2) && isAccessor(bind::fname(elem->right()))) {
+        matching[elem->right()] = elem->left();
+        return true;
+      }
+
+      else if ((elem->left()->arity() == 2) && isAccessor(bind::fname(elem->left()))) {
+        matching[elem->left()] = elem->right();
+        return true;
+      }
+      // TODO: HERE I CAN CHECK IF ACCESSOR, AND THEN DO THE REVERSE MATCHING, SO HEAD(SMTH) -> X, NOT X -> HEAD(SMTH)
       if ((elem->left()->arity() == 1) && !(isConstructor(bind::fname(elem->left())))) {
           matching[elem->left()] = elem->right();
           return true;
@@ -127,6 +139,11 @@ namespace ufo
       return std::find(constructors.begin(), constructors.end(), elem) != constructors.end();
     }
 
+
+    bool isAccessor(Expr elem) {
+      return std::find(accessors.begin(), accessors.end(), fname(elem)) != accessors.end();
+    }
+
     Expr createDestination(HornRuleExt chc) {
       int ind = values_inds[chc.dstRelation->left()];
       ExprVector types;
@@ -465,10 +482,8 @@ namespace ufo
           // add functions for filter variables here
           if (ignoreBaseVar) excludeBaseVar(cur, idxs);
           if (givePriority) givePriorityNonAdt(cur, idxs);
-           // outs() << *chc.dstRelation->left() << " " << idxs.size() << "\n";
           for (int i = idxs.size() - 1; i >= 0; --i) {
             buf[chc.dstRelation->left()] = idxs[i];
-            // outs() << *chc.dstRelation->left() << " " << idxs[i] << "\n";
             if (findInterpretations(idx + 1, buf))
               return true;
           }
@@ -481,7 +496,6 @@ namespace ufo
     bool solve() {
       // Order current uninterpreted predicate symbols
       for (auto & decl: decls) {
-        // outs() << *decl << "\n";
         ExprSet cur_decls;
         if (!orderDecls(decl, cur_decls))
           return false;
@@ -581,6 +595,7 @@ namespace ufo
     // ruleManager.print();
 
     ExprVector constructors;
+    ExprVector accessors;
 
     ExprSet& decls = ruleManager.decls;
 
@@ -589,7 +604,12 @@ namespace ufo
       adts.insert(a->last());
     }
 
-    CHCSolver sol (constructors, adts, efac, decls, ruleManager.extras, ruleManager.chcs,
+    for (auto & a : z3.getAdtAccessors()) {
+      accessors.push_back(regularizeQF(a));
+      adts.insert(a->last());
+    }
+
+    CHCSolver sol (constructors, accessors, adts, efac, decls, ruleManager.extras, ruleManager.chcs,
       givePriorityNonAdt, ignoreBaseVar);
     bool res = containsOp<ARRAY_TY>(conjoin(decls, efac)) ? sol.solveArr() : sol.solve();
     outs () << (res ? "sat\n" : "unknown\n");
diff --git a/include/deep/HornNonlin.hpp b/include/deep/HornNonlin.hpp
index ca929a4eb..1d507e9b8 100755
--- a/include/deep/HornNonlin.hpp
+++ b/include/deep/HornNonlin.hpp
@@ -108,8 +108,9 @@ namespace ufo
       for (auto c = lin.begin(); c != lin.end(); )
       {
         Expr cnj = *c;
-        if (isOpX<FAPP>(cnj) && isOpX<FDECL>(cnj->left()))
+        if (isOpX<FAPP>(cnj))
         {
+          assert(isOpX<FDECL>(cnj->left()));
           Expr rel = cnj->arg(0);
           addDecl(rel);
           srcRelations.push_back(rel);
diff --git a/include/ufo/Expr.hpp b/include/ufo/Expr.hpp
index 5cc4c686b..b67130833 100644
--- a/include/ufo/Expr.hpp
+++ b/include/ufo/Expr.hpp
@@ -1148,9 +1148,8 @@ namespace expr
   {
     if (expr->use_count () > 1)
       {
-	DagVisitCache::const_iterator cit 
-	  = cache.find (&*expr);
-	if (cit != cache.end ()) return cit->second;
+        DagVisitCache::const_iterator cit = cache.find (&*expr);
+        if (cit != cache.end ()) return cit->second;
       }
     
     
@@ -1163,39 +1162,37 @@ namespace expr
       res = va.getExpr ();
     else
       {
-	res = va.isChangeDoKidsRewrite () ? va.getExpr () : expr;
-	if (res->arity () > 0) 
-	  {
-	    bool changed = false;
-            std::vector<Expr> kids;
-
-	    for (ENode::args_iterator b = res->args_begin (), 
-		   e = res->args_end (); 
-		 b != e; ++b)
-	      {
-		Expr k = visit (v, *b, cache);
-		kids.push_back (k);
-		changed  = (changed || k.get () != *b);
-	      }
-	    
-	    if (changed)
-	      {
-		if (!res->isMutable ())
-		  res = res->getFactory ().mkNary (res->op (),
-						   kids.begin (),
-						   kids.end ());
-		else
-		  res->renew_args (kids.begin (), kids.end ());
-	      }
-	  }
+          res = va.isChangeDoKidsRewrite () ? va.getExpr () : expr;
+          if (res->arity () > 0)
+          {
+            bool changed = false;
+                std::vector<Expr> kids;
+
+            for (ENode::args_iterator b = res->args_begin (), e = res->args_end ();   b != e; ++b)
+              {
+                  Expr k = visit (v, *b, cache);
+                  kids.push_back (k);
+                  changed  = (changed || k.get () != *b);
+              }
+
+            if (changed)
+              {
+                if (!res->isMutable ())
+                  res = res->getFactory ().mkNary (res->op (),
+                                   kids.begin (),
+                                   kids.end ());
+                else
+                  res->renew_args (kids.begin (), kids.end ());
+              }
+          }
     
-	res = va.rewrite (res);
+        res = va.rewrite (res);
       }
 
     if (expr->use_count () > 1)
       {
-	expr->Ref ();
-	cache[&*expr] = res;
+        expr->Ref ();
+        cache[&*expr] = res;
       }
     
     return res;
@@ -2244,12 +2241,13 @@ namespace expr
       template <typename Range>
       Expr fapp (Expr fdecl, const Range &args)
       {
-	ExprVector _args;
-	_args.push_back (fdecl);
-	_args.insert (_args.end (), boost::begin (args), boost::end (args));
-	return mknary<FAPP> (_args);
+        ExprVector _args;
+        _args.push_back (fdecl);
+        _args.insert (_args.end (), boost::begin (args), boost::end (args));
+        return mknary<FAPP> (_args);
       }
 
+
       inline Expr fapp (Expr fdecl, Expr a0, Expr a1 = Expr(), 
 			Expr a2 = Expr())
       {
@@ -2285,10 +2283,9 @@ namespace expr
       
       template <typename T> bool isFdecl (Expr v)
       {
-	return isOpX<FDECL> (v) && isOpX<T> (rangeTy (v));
+        return isOpX<FDECL> (v) && isOpX<T> (rangeTy (v));
       }
-      
-      
+
       /** constant is an applied nullary function */
       template <typename T> bool isConst (Expr v)
       {
@@ -2360,27 +2357,27 @@ namespace expr
 
       struct FAPP_PS
       {
-	static inline void print (std::ostream &OS,
-				  int depth, 
-				  int brkt,
-				  const std::string &name,
-				  const std::vector<ENode*> &args)
-	{
-	  if (args.size () > 1) OS << "(";
+            static inline void print (std::ostream &OS,
+                          int depth,
+                          int brkt,
+                          const std::string &name,
+                          const std::vector<ENode*> &args)
+            {
+              if (args.size () > 1) OS << "(";
 
-	  // -- strip fdecl if there is one
-	  ENode *fname = args [0];
-	  if (isOpX<FDECL> (fname)) fname = fname->arg (0);
-	  fname->Print (OS, depth+2, false);
+              // -- strip fdecl if there is one
+              ENode *fname = args [0];
+              if (isOpX<FDECL> (fname)) fname = fname->arg (0);
+              fname->Print (OS, depth+2, false);
 
-	  for (unsigned i = 1; i < args.size (); ++i)
-	    {
-	      OS << " ";
-	      args [i]->Print (OS, depth+2, false);
-	    }
-	  
-	  if (args.size () > 1) OS << ")";
-	}
+              for (unsigned i = 1; i < args.size (); ++i)
+                {
+                  OS << " ";
+                  args [i]->Print (OS, depth+2, false);
+                }
+
+              if (args.size () > 1) OS << ")";
+            }
 	
       };
       
diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp
index c43980419..6fe0f3d0a 100644
--- a/include/ufo/Smt/Z3n.hpp
+++ b/include/ufo/Smt/Z3n.hpp
@@ -189,7 +189,6 @@ namespace ufo
   Expr z3_from_smtlib_file (Z &z3, const char *fname)
   {
       z3::context &ctx = z3.get_ctx ();
-
       Z3_ast_vector b = Z3_parse_smtlib2_file (ctx, fname, 0, NULL, NULL, 0, NULL, NULL);
       Z3_ast* args = new Z3_ast[Z3_ast_vector_size(ctx, b)];
 
@@ -286,6 +285,7 @@ namespace ufo
   protected:
     z3::context &get_ctx () { return ctx; }
     std::vector<Expr> adts;
+    std::vector<Expr> accessors;
 
     z3::ast toAst (Expr e)
     {
@@ -298,7 +298,7 @@ namespace ufo
 
       ast_expr_map seen;
       std::vector<std::string> adts_seen;
-      return U::unmarshal (a, get_efac (), cache.right, seen, adts_seen, adts);
+      return U::unmarshal (a, get_efac (), cache.right, seen, adts_seen, adts, accessors);
     }
 
     ExprFactory &get_efac () { return efac; }
@@ -349,6 +349,7 @@ namespace ufo
     }
 
     ExprVector& getAdtConstructors(){ return adts; }
+    ExprVector& getAdtAccessors(){ return accessors; }
 
     template <typename Range>
     std::string toSmtLibDecls (const Range &rng)
diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp
index 2f24d0b76..8bd24b8dc 100644
--- a/include/ufo/Smt/ZExprConverter.hpp
+++ b/include/ufo/Smt/ZExprConverter.hpp
@@ -207,9 +207,9 @@ namespace ufo
 	{
 
 	  z3::func_decl zfdecl (ctx,
-				reinterpret_cast<Z3_func_decl>
-				(static_cast<Z3_ast>
-				 (marshal (bind::fname (e), ctx, cache, seen))));
+                            reinterpret_cast<Z3_func_decl>
+                            (static_cast<Z3_ast>
+                             (marshal (bind::fname (e), ctx, cache, seen))));
 
 
 	  // -- marshall all arguments except for the first one
@@ -488,6 +488,7 @@ namespace ufo
         else if (isOp<ARRAY_MAP> (e))
         {
           Z3_func_decl fdecl = reinterpret_cast<Z3_func_decl> (args[0]);
+          printf("Func decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl)));
           res = Z3_mk_map (ctx, fdecl, e->arity ()-1, &args[1]);
         }
       }
@@ -506,13 +507,17 @@ namespace ufo
     }
   };
 
-  template <typename U>
+  static Expr left;
+  ExprVector subexpr;
+
+
+    template <typename U>
   struct BasicExprUnmarshal
   {
     template <typename C>
     static Expr unmarshal (const z3::ast &z,
 			   ExprFactory &efac, C &cache, ast_expr_map &seen,
-         std::vector<std::string> &adts_seen, std::vector<Expr> &adts)
+         std::vector<std::string> &adts_seen, std::vector<Expr> &adts, std::vector<Expr> &accessors)
     {
       z3::context &ctx = z.ctx ();
 
@@ -547,29 +552,40 @@ namespace ufo
           Expr domain, range;
 
 	  switch (Z3_get_sort_kind (ctx, sort))
-	    {
-	    case Z3_BOOL_SORT:
-	      return sort::boolTy (efac);
-	    case Z3_INT_SORT:
-	      return sort::intTy (efac);
-	    case Z3_REAL_SORT:
-	      return sort::realTy (efac);
-      case Z3_BV_SORT:
-        return bv::bvsort (Z3_get_bv_sort_size (ctx, sort), efac);
-      case Z3_ARRAY_SORT:
-        domain =
-          unmarshal (z3::ast (ctx,
-                              Z3_sort_to_ast
-                              (ctx, Z3_get_array_sort_domain (ctx, sort))),
-                     efac, cache, seen, adts_seen, adts);
-        range =
-          unmarshal (z3::ast (ctx,
-                              Z3_sort_to_ast
-                              (ctx, Z3_get_array_sort_range (ctx, sort))),
-                     efac, cache, seen, adts_seen, adts);
-        return sort::arrayTy (domain, range);
+      {
+        case Z3_BOOL_SORT:
+          return sort::boolTy (efac);
+        case Z3_INT_SORT:
+          return sort::intTy (efac);
+        case Z3_REAL_SORT:
+          return sort::realTy (efac);
+  case Z3_BV_SORT:
+    return bv::bvsort (Z3_get_bv_sort_size (ctx, sort), efac);
+  case Z3_ARRAY_SORT:
+    domain =
+      unmarshal (z3::ast (ctx,
+                          Z3_sort_to_ast
+                          (ctx, Z3_get_array_sort_domain (ctx, sort))),
+                 efac, cache, seen, adts_seen, adts, accessors);
+    range =
+      unmarshal (z3::ast (ctx,
+                          Z3_sort_to_ast
+                          (ctx, Z3_get_array_sort_range (ctx, sort))),
+                 efac, cache, seen, adts_seen, adts, accessors);
+    return sort::arrayTy (domain, range);
       case Z3_DATATYPE_SORT:
         {
+            unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort);
+            while (num > 0) {
+                num--;
+                auto c = Z3_get_datatype_sort_constructor(ctx, sort, num);
+                unsigned num_accessors = Z3_get_domain_size(ctx, c);
+
+                while(num_accessors > 0){
+                    num_accessors--;
+                    auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors);
+                }
+            }
           std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort));
           Expr adt_name = mkTerm<std::string> (name, efac);
           if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end())
@@ -579,12 +595,12 @@ namespace ufo
             {
               Z3_func_decl decl = Z3_get_datatype_sort_constructor(ctx, sort, i);
               Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl);
-              adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts));
+              adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts, accessors));
             }
           }
           return sort::adTy (adt_name);
         }
-	    default:
+        default:
         std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort));
         Expr adt_name = mkTerm<std::string> (name, efac);
         if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end())
@@ -592,54 +608,55 @@ namespace ufo
           adts_seen.push_back(name);
         }
         return sort::adTy (adt_name);
-	    }
-	}
+    }
+}
       else if (kind == Z3_VAR_AST)
 	{
 	  unsigned idx = Z3_get_index_value (ctx, z);
           z3::ast zsort (ctx, Z3_sort_to_ast (ctx, Z3_get_sort (ctx, z)));
-          Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts);
+          Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts, accessors);
           return bind::bvar (idx, sort);
 	}
 
-      else if (kind == Z3_FUNC_DECL_AST)
+    else if (kind == Z3_FUNC_DECL_AST)
 	{
-            {
-                typename C::const_iterator it = cache.find (z);
-                if (it != cache.end ()) return it->second;
-            }
-	  Z3_func_decl fdecl = Z3_to_func_decl (ctx, z);
+      {
+        typename C::const_iterator it = cache.find (z);
+        if (it != cache.end ()) return it->second;
+      }
+      Z3_func_decl fdecl = Z3_to_func_decl (ctx, z);
 
-	  Z3_symbol symname = Z3_get_decl_name (ctx, fdecl);
-          
-          Expr name;
-          switch (Z3_get_symbol_kind (ctx, symname))
-          {
+//       printf("Func decl ast: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl)));
+
+      Z3_symbol symname = Z3_get_decl_name (ctx, fdecl);
+
+      Expr name;
+      std::string st = Z3_get_symbol_string(ctx, symname) ;
+      switch (Z3_get_symbol_kind (ctx, symname)) {
           case Z3_STRING_SYMBOL:
             name = mkTerm<std::string> (Z3_get_symbol_string (ctx, symname), efac);
             break;
           case Z3_INT_SYMBOL:
             name = mkTerm<mpz_class> (Z3_get_symbol_int (ctx, symname), efac);
             break;
-          }
-          assert (name);
-
-	  ExprVector type;
-	  for (unsigned p = 0; p < Z3_get_domain_size (ctx, fdecl); ++p)
-	    {
-	      Z3_sort sort = Z3_get_domain  (ctx, fdecl, p);
-	      type.push_back
-		(unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)),
-			    efac, cache, seen, adts_seen, adts));
-	    }
+      }
+      assert (name);
 
-	  type.push_back
-	    (unmarshal (z3::ast (ctx,
-				 Z3_sort_to_ast (ctx,
-						 Z3_get_range (ctx, fdecl))),
-				     efac, cache, seen, adts_seen, adts));
+      ExprVector type;
+      for (unsigned p = 0; p < Z3_get_domain_size (ctx, fdecl); ++p)
+        {
+          Z3_sort sort = Z3_get_domain  (ctx, fdecl, p);
+          type.push_back
+        (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)),
+                efac, cache, seen, adts_seen, adts, accessors));
+        }
 
-	  return bind::fdecl (name, type);
+      type.push_back
+        (unmarshal (z3::ast (ctx,
+                 Z3_sort_to_ast (ctx,
+                         Z3_get_range (ctx, fdecl))),
+                     efac, cache, seen, adts_seen, adts, accessors));
+      return bind::fdecl (name, type);
 	}
       else if (kind == Z3_QUANTIFIER_AST)
       {
@@ -652,12 +669,13 @@ namespace ufo
                                                Z3_get_quantifier_bound_name (ctx, z, i),
                                                0, nullptr,
                                                Z3_get_quantifier_bound_sort (ctx, z, i));
+
           z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, decl));
-          args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts));
+          args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors));
           assert (args.back ().get ());
         }
         args.push_back (unmarshal (z3::ast (ctx, Z3_get_quantifier_body (ctx, z)),
-                                   efac, cache, seen, adts_seen, adts));
+                                   efac, cache, seen, adts_seen, adts, accessors));
         return Z3_is_quantifier_forall (ctx, z) ?
           mknary<FORALL> (args) : mknary<EXISTS> (args);
       }
@@ -676,36 +694,36 @@ namespace ufo
 	  assert (Z3_get_app_num_args (ctx, app) == 1);
 	  return mk<NEG> (unmarshal
 			  (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-				    efac, cache, seen, adts_seen, adts));
+				    efac, cache, seen, adts_seen, adts, accessors));
     	}
       if (dkind == Z3_OP_UMINUS)
 	return mk<UN_MINUS> (unmarshal
 			     (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-			      efac, cache, seen, adts_seen, adts));
+			      efac, cache, seen, adts_seen, adts, accessors));
 
       // XXX ignore to_real and to_int operators
       if (dkind == Z3_OP_TO_REAL || dkind == Z3_OP_TO_INT)
         return unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                          efac, cache, seen, adts_seen, adts);
+                          efac, cache, seen, adts_seen, adts, accessors);
       
       if (dkind == Z3_OP_BNOT)
         return mk<BNOT> (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                                    efac, cache, seen, adts_seen, adts));
+                                    efac, cache, seen, adts_seen, adts, accessors));
       if (dkind == Z3_OP_BNEG)
         return mk<BNEG> (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                                    efac, cache, seen, adts_seen, adts));
+                                    efac, cache, seen, adts_seen, adts, accessors));
       if (dkind == Z3_OP_BREDAND)
         return mk<BREDAND> (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                                       efac, cache, seen, adts_seen, adts));
+                                       efac, cache, seen, adts_seen, adts, accessors));
       if (dkind == Z3_OP_BREDOR)
         return mk<BREDOR> (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                                      efac, cache, seen, adts_seen, adts));
+                                      efac, cache, seen, adts_seen, adts, accessors));
       if (dkind == Z3_OP_SIGN_EXT || dkind == Z3_OP_ZERO_EXT)
       {
         Expr sort = bv::bvsort (Z3_get_bv_sort_size (ctx, Z3_get_sort (ctx, z)), 
                                 efac);
         Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                              efac, cache, seen, adts_seen, adts);
+                              efac, cache, seen, adts_seen, adts, accessors);
         switch (dkind)
         {
         case Z3_OP_SIGN_EXT:
@@ -719,7 +737,7 @@ namespace ufo
       if (dkind == Z3_OP_EXTRACT)
       {
         Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)),
-                              efac, cache, seen, adts_seen, adts);
+                              efac, cache, seen, adts_seen, adts, accessors);
 
         Z3_func_decl d = Z3_get_app_decl (ctx, app);
         unsigned high = Z3_get_decl_int_parameter (ctx, d, 0);
@@ -733,7 +751,7 @@ namespace ufo
         z3::ast zdecl 
           (ctx, Z3_func_decl_to_ast (ctx, 
                                      Z3_get_as_array_func_decl (ctx, z)));
-        return mk<AS_ARRAY> (unmarshal (zdecl, efac, cache, seen, adts_seen, adts));
+        return mk<AS_ARRAY> (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors));
       }
       {
 	typename C::const_iterator it = cache.find (z);
@@ -747,73 +765,132 @@ namespace ufo
       
       Expr e;
       ExprVector args;
-      for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++)
-        args.push_back (unmarshal
-              (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts));
+      for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++){
+            // TODO: Disequality, constructor inside constructor(maybe), IF then else
+          if(dkind == Z3_OP_EQ && i == 1 && Z3_get_decl_kind (ctx, Z3_get_app_decl (ctx, Z3_to_app(ctx, z3::ast(ctx, Z3_get_app_arg(ctx, app, i))))) == Z3_OP_DT_CONSTRUCTOR){
+              left = args[0];
+          }
+          args.push_back (unmarshal
+                                  (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts, accessors));
+      }
+
 
-      /** newly introduced Z3 symbol */
-      if (dkind == Z3_OP_UNINTERPRETED || dkind == Z3_OP_DT_CONSTRUCTOR)
+        /** newly introduced Z3 symbol */
+      // TODO: Bind the accessor variable
+      if (dkind == Z3_OP_DT_CONSTRUCTOR )
       {
-        Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl),
-                  efac, cache, seen, adts_seen, adts), args);
-        // -- XXX maybe use seen instead. not sure what is best.
-        cache.insert (typename C::value_type (z, res));
-        return res;
+            if (left != NULL) {
+                Z3_sort sort = Z3_get_sort (ctx, z);
+                unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort);
+                while (num > 0) {
+                   num--;
+                   auto c = Z3_get_datatype_sort_constructor(ctx, sort, num);
+                   unsigned num_accessors = Z3_get_domain_size(ctx, c);
+                   if(c != fdecl){
+                       continue;
+                   }
+
+                   while(num_accessors > 0){
+                        num_accessors--;
+                        auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors);
+                        ExprVector eq;
+                        // Put value from the constructor into equality
+                        eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as),
+                                                            efac, cache, seen, adts_seen, adts, accessors), { left }));
+                        eq.push_back (args[num_accessors]);
+
+                        accessors.push_back(bind::fname((unmarshal (z3::func_decl (ctx, as),
+                                                                   efac, cache, seen, adts_seen, adts, accessors))));
+                        // accessor(data) = value
+                        subexpr.push_back(mknary<EQ> (eq.begin(), eq.end()));
+                   }
+                }
+            }
+
+            Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl),
+                                            efac, cache, seen, adts_seen, adts, accessors), args);
+            cache.insert (typename C::value_type (z, res));
+            left = NULL;
+            return res;
       }
 
-      switch (dkind)
+      if (dkind == Z3_OP_UNINTERPRETED) {
+            Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl),
+                      efac, cache, seen, adts_seen, adts, accessors), args);
+            // -- XXX maybe use seen instead. not sure what is best.
+            cache.insert (typename C::value_type (z, res));
+            return res;
+     }
+
+      if (dkind == Z3_OP_DT_ACCESSOR) {
+          Z3_sort srt = Z3_get_sort(ctx, z);
+          Z3_func_decl acc = Z3_get_datatype_sort_constructor_accessor(ctx, srt,1,1);
+          Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl),
+                                            efac, cache, seen, adts_seen, adts, accessors), args);
+          accessors.push_back(bind::fname(res));
+//           -- XXX maybe use seen instead. not sure what is best.
+          cache.insert (typename C::value_type (z, res));
+          return res;
+      }
+    switch (dkind)
 	{
-	case Z3_OP_ITE:
-	  e = mknary<ITE> (args.begin (), args.end ());
-	  break;
-	case Z3_OP_AND:
-	  e = mknary<AND> (args.begin(), args.end());
-	  break;
-	case Z3_OP_OR:
-	  e =  mknary<OR> (args.begin(), args.end());
-	  break;
-	case Z3_OP_XOR:
-	  e = mknary<XOR> (args.begin(), args.end());
-	  break;
-	case Z3_OP_IFF:
-	  e =  mknary<IFF> (args.begin(), args.end());
-	  break;
-	case Z3_OP_IMPLIES:
-	  e =  mknary<IMPL> (args.begin(), args.end());
-	  break;
-	case Z3_OP_EQ:
-	  e =  mknary<EQ> (args.begin(), args.end());
-	  break;
-	case Z3_OP_LT:
-	  e =  mknary<LT> (args.begin(), args.end());
-	  break;
-	case Z3_OP_GT:
-	  e =  mknary<GT> (args.begin(), args.end());
-	  break;
-	case Z3_OP_LE:
-	  e =  mknary<LEQ> (args.begin(), args.end());
-	  break;
-	case Z3_OP_GE:
-	  e =  mknary<GEQ> (args.begin(), args.end());
-	  break;
-	case Z3_OP_ADD:
-	  e =  mknary<PLUS> (args.begin(), args.end());
-	  break;
-	case Z3_OP_SUB:
-	  e =  mknary<MINUS> (args.begin(), args.end());
-	  break;
-	case Z3_OP_MUL:
-	  e =  mknary<MULT> (args.begin(), args.end());
-	  break;
-	case Z3_OP_DIV:
-	  e = mknary<DIV> (args.begin(), args.end());
-	  break;
+        case Z3_OP_ITE:
+          e = mknary<ITE> (args.begin (), args.end ());
+          break;
+        case Z3_OP_AND:
+          e = mknary<AND> (args.begin(), args.end());
+          break;
+        case Z3_OP_OR:
+          e =  mknary<OR> (args.begin(), args.end());
+          break;
+        case Z3_OP_XOR:
+          e = mknary<XOR> (args.begin(), args.end());
+          break;
+        case Z3_OP_IFF:
+          e =  mknary<IFF> (args.begin(), args.end());
+          break;
+        case Z3_OP_IMPLIES:
+          e =  mknary<IMPL> (args.begin(), args.end());
+          break;
+        case Z3_OP_EQ:
+          e =  mknary<EQ> (args.begin(), args.end());
+          if(subexpr.size() > 0){
+              subexpr.push_back(e);
+
+              e = mknary<AND>(subexpr.begin(), subexpr.end());
+              subexpr.clear();
+          }
+          break;
+        case Z3_OP_LT:
+          e =  mknary<LT> (args.begin(), args.end());
+          break;
+        case Z3_OP_GT:
+          e =  mknary<GT> (args.begin(), args.end());
+          break;
+        case Z3_OP_LE:
+          e =  mknary<LEQ> (args.begin(), args.end());
+          break;
+        case Z3_OP_GE:
+          e =  mknary<GEQ> (args.begin(), args.end());
+          break;
+        case Z3_OP_ADD:
+          e =  mknary<PLUS> (args.begin(), args.end());
+          break;
+        case Z3_OP_SUB:
+          e =  mknary<MINUS> (args.begin(), args.end());
+          break;
+        case Z3_OP_MUL:
+          e =  mknary<MULT> (args.begin(), args.end());
+          break;
+        case Z3_OP_DIV:
+          e = mknary<DIV> (args.begin(), args.end());
+          break;
         case Z3_OP_IDIV:
           e = mknary<IDIV> (args.begin (), args.end ());
           break;
-	case Z3_OP_MOD:
-	  e = mknary<MOD> (args.begin (), args.end ());
-	  break;
+        case Z3_OP_MOD:
+          e = mknary<MOD> (args.begin (), args.end ());
+          break;
         case Z3_OP_REM:
           e = mknary<REM> (args.begin (), args.end ());
           break;
@@ -827,7 +904,7 @@ namespace ufo
             Expr domain = unmarshal
               (z3::ast (ctx, Z3_sort_to_ast (ctx,
                                              Z3_get_array_sort_domain (ctx, sort))),
-               efac, cache, seen, adts_seen, adts);
+               efac, cache, seen, adts_seen, adts, accessors);
             
             e = op::array::constArray (domain, args[0]);
           }