Skip to content

Commit a865074

Browse files
committed
Fix cvc5 sort converter
1 parent dbb8531 commit a865074

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -820,6 +820,8 @@ open class KCvc5ExprConverter(
820820
sort.isBitVector -> mkBvSort(sort.bitVectorSize.toUInt())
821821
sort.isInteger -> intSort
822822
sort.isReal -> realSort
823+
sort.isString -> stringSort
824+
sort.isRegExp -> regexSort
823825
sort.isArray -> mkArrayAnySort(
824826
domain = convertArrayDomainSort(tm.sortOp(sort) { arrayIndexSort }),
825827
range = tm.sortOp(sort) { arrayElementSort }.convertSort()

0 commit comments

Comments
 (0)