Bug: Tree Automizer returns UNSAT for SAT instance

[kensingRichardt]

Basic Info

• Version: 0.2.4-dev-0e0057c
• Java Version: 11.0.24
• Settings: TreeAutomizerHopcroftMinimization.epf
• Toolchain: TreeAutomizer.xml
• The log file is attached
  If I invoke Ultimate Tree Automizer on the following file, I get UNSAT.

(set-logic HORN)

(assert 
    (exists ((x Int)) 
      (= 0 x)
    )
)

(check-sat)

However this is clearly a SAT-instance.
log.txt

[maul-esel]

Thank you for the bug report.

I've been able to reproduce the bug, and a bit of debugging shows:

• During parsing, Ultimate introduces a Skolem constant for the quantified variable.
• Unfortunately, TreeAutomizer does not have any support for Skolem functions (the parser introduces them because our other CHC solver, UltimateUniHorn, has some support).
• TreeAutomizer incorrectly treats the Skolem constant similar to a universally-quantified variable, and thus reports UNSAT.

Handling such examples correctly is non-trivial effort, as we have to add a whole new feature to TreeAutomizer. So for now, I've modified TreeAutomizer to report UNKNOWN in such cases.

[maul-esel]

I've opened #679 to keep track of the missing feature, and will close this bug report now.