diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index f13b2cbb8..dd18f865c 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -22,12 +22,14 @@ Notes:
 #include"stream_buffer.h"
 #include"symbol.h"
 #include"trace.h"
+#include<sstream>
 
 void register_z3_replayer_cmds(z3_replayer & in);
 
+
 void throw_invalid_reference() {
     TRACE("z3_replayer", tout << "invalid argument reference\n";);
-    throw z3_replayer_exception("invalid argument reference");
+    throw z3_replayer_exception("invalid argument reference1");
 }
 
 struct z3_replayer::imp {
@@ -46,6 +48,36 @@ struct z3_replayer::imp {
 
     enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY };
 
+    char const* kind2string(value_kind k) const {
+        switch (k) {
+        case INT64: return "int64";
+        case UINT64: return "uint64";
+        case DOUBLE: return "double";
+        case STRING: return "string";
+        case SYMBOL: return "symbol";
+        case OBJECT: return "object";
+        case UINT_ARRAY: return "uint_array";
+        case INT_ARRAY: return "int_array";
+        case SYMBOL_ARRAY: return "symbol_array";
+        case OBJECT_ARRAY: return "object_array";
+        default: UNREACHABLE(); return "unknown";
+        }
+    }
+
+
+    void check_arg(unsigned pos, value_kind k) const {
+        if (pos >= m_args.size()) {
+            TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
+            throw z3_replayer_exception("invalid argument reference2");
+        }
+        if (m_args[pos].m_kind != k) {
+            std::stringstream strm;
+            strm << "expecting " << kind2string(k) << " at position " 
+                 << pos << " but got " << kind2string(m_args[pos].m_kind);
+            throw z3_replayer_exception(strm.str().c_str());
+        }
+    }
+
     struct value { 
         value_kind m_kind;
         union {
@@ -467,8 +499,7 @@ struct z3_replayer::imp {
                 next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
                 unsigned pos = static_cast<unsigned>(m_uint64);
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "* " << m_ptr << " " << pos << "\n";);
-                if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-                    throw_invalid_reference();
+                check_arg(pos, OBJECT);
                 m_heap.insert(m_ptr, m_args[pos].m_obj);
                 break;
             }
@@ -477,8 +508,7 @@ struct z3_replayer::imp {
                 // @ obj_id array_pos idx
                 next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
                 unsigned pos = static_cast<unsigned>(m_uint64);
-                if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY)
-                    throw_invalid_reference();
+                check_arg(pos, OBJECT_ARRAY);
                 unsigned aidx = static_cast<unsigned>(m_args[pos].m_uint);
                 ptr_vector<void> & v = m_obj_arrays[aidx];
                 skip_blank(); read_uint64();
@@ -503,77 +533,65 @@ struct z3_replayer::imp {
     }
 
     int get_int(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return static_cast<int>(m_args[pos].m_int);
     }
 
     __int64 get_int64(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return m_args[pos].m_int;
     }
 
     unsigned get_uint(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return static_cast<unsigned>(m_args[pos].m_uint);
     }
 
     __uint64 get_uint64(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return m_args[pos].m_uint;
     }
 
     double get_double(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != DOUBLE)
-            throw_invalid_reference();
+        check_arg(pos, DOUBLE);
         return m_args[pos].m_double;
     }
 
     Z3_string get_str(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != STRING)
-            throw_invalid_reference();
+        check_arg(pos, STRING);
         return m_args[pos].m_str;
     }
 
     Z3_symbol get_symbol(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL)
-            throw_invalid_reference();
+        check_arg(pos, SYMBOL);
         return reinterpret_cast<Z3_symbol>(const_cast<char*>(m_args[pos].m_str));
     }
 
     void * get_obj(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT);
         return m_args[pos].m_obj;
     }
 
     unsigned * get_uint_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, UINT_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         return m_unsigned_arrays[idx].c_ptr();
     }
 
     int * get_int_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, INT_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         return m_int_arrays[idx].c_ptr();
     }
 
     Z3_symbol * get_symbol_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, SYMBOL_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         return m_sym_arrays[idx].c_ptr();
     }
 
     void ** get_obj_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         ptr_vector<void> const & v = m_obj_arrays[idx];
         TRACE("z3_replayer_bug", tout << "pos: " << pos << ", idx: " << idx << " size(): " << v.size() << "\n";
@@ -582,38 +600,32 @@ struct z3_replayer::imp {
     }
 
     int * get_int_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return reinterpret_cast<int*>(&(m_args[pos].m_int));
     }
 
     __int64 * get_int64_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return &(m_args[pos].m_int);
     }
 
     unsigned * get_uint_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return reinterpret_cast<unsigned*>(&(m_args[pos].m_uint));
     }
 
     __uint64 * get_uint64_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return &(m_args[pos].m_uint);
     }
 
     Z3_string * get_str_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != STRING)
-            throw_invalid_reference();
+        check_arg(pos, STRING);
         return &(m_args[pos].m_str);
     }
 
     void ** get_obj_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT);
         return &(m_args[pos].m_obj);
     }