theory of arithmetic isn't being loaded properly
Closed this issue · 0 comments
mtrberzi commented
(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)