From d2b78bbd793b27bc036233b69c61edbb00d0d8c8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:39:15 -0800
Subject: [PATCH] [sledge] Improve term printing, avoid misidentification of
 string constants

Reviewed By: jvillard

Differential Revision: D24920760

fbshipit-source-id: 1c139403d
---
 sledge/src/fol/trm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index d292fe294..e28787280 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -151,7 +151,8 @@ end = struct
             pf "%S"
               (String.init (Array.length xs) ~f:(fun i ->
                    match xs.(i) with
-                   | Sized {seq= Z c} -> Char.of_int_exn (Z.to_int c)
+                   | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o ->
+                       Char.of_int_exn (Z.to_int c)
                    | _ -> raise_notrace Not_a_string ))
           with _ -> pf "(%a)" (Array.pp "@,^" pp) xs )
       | Apply (f, [||]) -> pf "%a" Funsym.pp f