diff --git a/sl/glconf.cc b/sl/glconf.cc
index 4dce15563..db077f894 100644
--- a/sl/glconf.cc
+++ b/sl/glconf.cc
@@ -195,6 +195,12 @@ void handleNoErrorRecovery(const string &name, const string &value)
     data.errorRecoveryMode = /* no_error_recovery */ 0;
 }
 
+void handleFullErrorRecovery(const string &name, const string &value)
+{
+    assumeNoValue(name, value);
+    data.errorRecoveryMode = /* full_error_recovery */ 2;
+}
+
 void handleVerifierErrorIsError(const string &name, const string &value)
 {
     assumeNoValue(name, value);
@@ -244,6 +250,7 @@ ConfigStringParser::ConfigStringParser()
     tbl_["error_label"]             = handleErrorLabel;
     tbl_["exit_leaks"]              = handleExitLeaks;
     tbl_["forbid_heap_replace"]     = handleForbidHeapReplace;
+    tbl_["full_error_recovery"]     = handleFullErrorRecovery;
     tbl_["int_arithmetic_limit"]    = handleIntArithmeticLimit;
     tbl_["join_on_loop_edges_only"] = handleJoinOnLoopEdgesOnly;
     tbl_["memleak_is_error"]        = handleMemLeakIsError;
diff --git a/sl/symexec.cc b/sl/symexec.cc
index 6c230bd64..47a6563bf 100644
--- a/sl/symexec.cc
+++ b/sl/symexec.cc
@@ -512,7 +512,7 @@ void SymExecEngine::execCondInsn()
     }
 
     const EValueOrigin origin = sh.valOrigin(val);
-    if (VO_DEREF_FAILED == origin) {
+    if (GlConf::data.errorRecoveryMode < 2 && VO_DEREF_FAILED == origin) {
         // error should have been already emitted
         CL_DEBUG_MSG(lw_, "ignored VO_DEREF_FAILED");
         return;
diff --git a/sl/symjoin.cc b/sl/symjoin.cc
index cc49c5c0a..7d886e653 100644
--- a/sl/symjoin.cc
+++ b/sl/symjoin.cc
@@ -643,7 +643,8 @@ EValueOrigin joinOrigin(const EValueOrigin vo1, const EValueOrigin vo2)
         // use any
         return vo2;
 
-    if (VO_DEREF_FAILED == vo1 || VO_DEREF_FAILED == vo2)
+    if (GlConf::data.errorRecoveryMode < 2
+            && (VO_DEREF_FAILED == vo1 || VO_DEREF_FAILED == vo2))
         // keep the error recovery as cheap as possible
         return VO_DEREF_FAILED;
 
diff --git a/sl/symproc.cc b/sl/symproc.cc
index 9bc0dfecb..84bb49e15 100644
--- a/sl/symproc.cc
+++ b/sl/symproc.cc
@@ -1389,7 +1389,8 @@ void SymExecCore::execFree(
             // fall through!
 
         case VT_UNKNOWN:
-            if (VO_DEREF_FAILED == sh_.valOrigin(val))
+            if (GlConf::data.errorRecoveryMode < 2
+                    && VO_DEREF_FAILED == sh_.valOrigin(val))
                 return;
 
             CL_ERROR_MSG(lw_, "invalid " << fnc);
@@ -1472,17 +1473,34 @@ void SymExecCore::execStackRestore()
     }
 }
 
-bool lhsFromOperand(FldHandle *pLhs, SymProc &proc, const struct cl_operand &op)
+bool SymProc::lhsFromOperand(FldHandle *pLhs, const struct cl_operand &op)
 {
     if (seekRefAccessor(op.accessor))
         CL_BREAK_IF("lhs not an l-value");
 
-    *pLhs = proc.fldByOperand(op);
-    if (FLD_DEREF_FAILED == pLhs->fieldId())
-        return false;
+    *pLhs = this->fldByOperand(op);
+    if (FLD_DEREF_FAILED != pLhs->fieldId()) {
+        // propagate the field returned by fldByOperand()
+        CL_BREAK_IF(!pLhs->isValidHandle());
+        return true;
+    }
 
-    CL_BREAK_IF(!pLhs->isValidHandle());
-    return true;
+    if (2 <= GlConf::data.errorRecoveryMode) {
+        // if the dereference failed due to out of range (or unknown) offset,
+        // try to resolve the allocated object and invalidate its contents in
+        // order to detect more errors in one run with full error recovery
+        const TObjId obj = this->objByVar(op);
+        if (sh_.isValid(obj)) {
+            const UniformBlock ub = {
+                /* off      */  0,
+                /* size     */  sh_.objSize(obj).hi,
+                /* tplValue */  sh_.valCreate(VT_UNKNOWN, VO_UNKNOWN)
+            };
+            sh_.writeUniformBlock(obj, ub);
+        }
+    }
+
+    return false;
 }
 
 void SymExecCore::execStackAlloc(
@@ -1491,7 +1509,7 @@ void SymExecCore::execStackAlloc(
 {
     // resolve lhs
     FldHandle lhs;
-    if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs))
+    if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs))
         // error alredy emitted
         return;
 
@@ -1502,7 +1520,7 @@ void SymExecCore::execStackAlloc(
         return;
     }
 
-    // now create an annonymous stack object
+    // now create an anonymous stack object
     const CallInst callInst(this->bt_);
     const TObjId obj = sh_.stackAlloc(size, callInst);
 
@@ -1531,8 +1549,8 @@ void SymExecCore::execHeapAlloc(
     // resolve lhs
     FldHandle lhs;
     const struct cl_operand &opLhs = insn.operands[/* dst */ 0];
-    if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs))
-        // error alredy emitted
+    if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs))
+        // error already emitted
         return;
 
     if (ep_.oomSimulation || /* malloc(0) may return NULL */ !size.hi) {
@@ -1649,7 +1667,7 @@ void SymExecCore::execHeapRealloc(
     // resolve lhs
     FldHandle lhs;
     const struct cl_operand &opLhs = insn.operands[/* dst */ 0];
-    if (CL_OPERAND_VOID != opLhs.code && !lhsFromOperand(&lhs, *this, opLhs))
+    if (CL_OPERAND_VOID != opLhs.code && !this->lhsFromOperand(&lhs, opLhs))
         // error alredy emitted
         return;
 
@@ -2841,7 +2859,7 @@ void SymExecCore::execOp(const CodeStorage::Insn &insn)
     // resolve lhs
     FldHandle lhs;
     const struct cl_operand &dst = insn.operands[/* dst */ 0];
-    if (!lhsFromOperand(&lhs, *this, dst))
+    if (!this->lhsFromOperand(&lhs, dst))
         // error alredy emitted
         return;
 
diff --git a/sl/symproc.hh b/sl/symproc.hh
index 88ae8cdf3..5f1d9946b 100644
--- a/sl/symproc.hh
+++ b/sl/symproc.hh
@@ -125,10 +125,13 @@ class SymProc {
         }
 
     public:
-        /// obtain a heap object corresponding to the given operand
+        /// obtain a field corresponding to the given operand
         FldHandle fldByOperand(const struct cl_operand &op);
 
-        /// obtain a heap value corresponding to the given operand
+        /// obtain a left-hand-side field corresponding to the given operand
+        bool lhsFromOperand(FldHandle *pLhs, const struct cl_operand &op);
+
+        /// obtain a SymHeap value corresponding to the given operand
         TValId valFromOperand(const struct cl_operand &op);
 
         /// resolve Fnc uid from the given operand, return true on success