about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h10
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 3112495d..376ffe25 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -182,7 +182,7 @@ MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root,
     if (!hashed) {
       un_expr = evaluate(_solver,
                          metaSMT::logic::Array::store(
-                             getArrayForUpdate(root, un->next),
+                             getArrayForUpdate(root, un->next.get()),
                              construct(un->index, 0), construct(un->value, 0)));
       _arr_hash.hashUpdateNodeExpr(un, un_expr);
     }
@@ -680,10 +680,10 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
     assert(re && re->updates.root);
     *width_out = re->updates.root->getRange();
     // FixMe call method of Array
-    res = evaluate(_solver,
-                   metaSMT::logic::Array::select(
-                       getArrayForUpdate(re->updates.root, re->updates.head),
-                       construct(re->index, 0)));
+    res = evaluate(_solver, metaSMT::logic::Array::select(
+                                getArrayForUpdate(re->updates.root,
+                                                  re->updates.head.get()),
+                                construct(re->index, 0)));
     break;
   }