mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
char sort
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
170ef1dcca
commit
592c53e46d
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue