UnitTestBot / ksmt

Kotlin/Java API for various SMT solvers
https://ksmt.io/
Apache License 2.0
30 stars 14 forks source link

Yices model doesn't collect all uninterpreted sort values #160

Open Bupaheh opened 6 months ago

Bupaheh commented 6 months ago

In the following example sortValues doesn't contain value

with(KContext()) {
    KYicesSolver(this).use { solver ->
        val sort = mkUninterpretedSort("sort")

        val value = mkUninterpretedSortValue(sort, 0)
        val a by sort

        solver.assert(a neq value)
        solver.check()

        val model = solver.model()
        val sortValues = model.uninterpretedSortUniverse(sort)!!

        println(value in sortValues)
    }
}