From 4b8a421e32764f8f20d19d05147516faabb82bf3 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 16 Oct 2017 09:10:40 +0100
Subject: [PATCH] Make get_array return array of unknown expr

This is in the case where super_get does not anything about the array we
give it.
This is necessary so that the string solver returns an array of the
correct size, if the size is the only thing we know about the string.

Add warning message in the case where the symbol is unknown to super_get
---
 src/solvers/refinement/string_refinement.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 71ba0de8338..a3da3b053f3 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -733,6 +733,16 @@ static optionalt<exprt> get_array(
       ret.move_to_operands(arr_val.operands()[i]);
     return ret;
   }
+  else if(arr_val.id() == ID_symbol)
+  {
+    stream << "(sr::get_array) warning: symbol "
+           << to_symbol_expr(arr_val).get_identifier()
+           << " not found by super_get" << eom;
+    // `super_get` does not know anything about this array so we make one up
+    for(size_t i = 0; i < n; i++)
+      ret.copy_to_operands(exprt(ID_unknown, arr_val.type().subtype()));
+    return ret;
+  }
   else
     return {};
 }