From 592c53e46dfc7992b300217f5d3e516724e26d91 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 23 Aug 2021 20:45:26 -0700
Subject: [PATCH] char sort

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_ast.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index d5e8a4073..4b4574b65 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -720,7 +720,7 @@ extern "C" {
             return Z3_RE_SORT;
         }
 	else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) {
-            return Z3_SEQ_SORT;
+            return Z3_CHAR_SORT;
         }
         else {
             return Z3_UNKNOWN_SORT;