Skip to content

:smtlib2_compliant setting makes the benchmark unknown #6969

Closed
@LeventErkok

Description

@LeventErkok

For the attached benchmark, z3 currently produces unknown.

However, if I comment out the first line in it, which is merely:

(set-option :smtlib2_compliant true)

then I get a sat answer.

I'm curious why there's this discrepancy; I thought the compliance only impacted what subset of smtlib2 was accepted, not how the solver behaved.

Furthermore, this seems to be a regression since z3 compiled on August 27 of this year produces sat on this benchmark.

compliant_unknown.txt

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions