mtrberzi/z3

theory of arithmetic isn't being loaded properly

Closed this issue · 0 comments

(set-logic QF_S)
(assert (< (Length "abc") 0))
(check-sat)

crashes with
(error "line X column Y: unknown function/constant <")
which would imply that the arithmetic theory isn't being initialized, because < certainly exists if I do (set-logic QF_LIA)