From 27765ee0f4309b22a5f141117a4aee11a342ac66 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Oct 2019 09:54:07 -0700
Subject: [PATCH] add stub for #2522

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/java/Expr.java | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 4df0f90a4..d1d554b54 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1290,6 +1290,22 @@ public class Expr extends AST
 	return Native.getString(getContext().nCtx(), getNativeObject());
     }
 
+    /**
+     * TBD: sketch for #2522, 'Pointer' seems deprecated and instead 
+     * approach seems to be around Set/Get CharArrayRegion and updating Native.cpp
+     * code generation to produce the char[].
+     * 
+    public char[] getNativeString()
+    {
+        Native.IntPtr len = new Native.IntPtr();
+        long s = Native.getLstring(getContext().nCtx(), getNativeObject(), len);
+        char[] result = new char[len.value];
+        Pointer ptr = Pointer.createConstant(s);
+        for (int i = 0; i < len.value; ++i) result[i] = ptr.getChar(i);
+        return result;
+    }
+    */
+
     /**
      * Check whether expression is a concatenation
      * @return a boolean