search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
374 stars 48 forks source link

The exists/forall solver failed: unsupported term #517

Open Heaven2024 opened 5 months ago

Heaven2024 commented 5 months ago

Hi Yices 2.6.4 Copyright SRI International. Linked with GMP 6.2.1 ubuntu:20.04

When using yices2 to solve quantifiers, I encountered a problem:

(set-logic LIA)
(declare-fun i0 () Int)
(assert (forall ((q22 Int)) (or (< q22 (abs i0)) (> q22 (abs i0)))))
(check-sat)

info:
(error "the exists/forall solver failed: unsupported term")

For the solution of quantifiers, correct processing will only be performed when the judgment logic is >. When = or< are encountered, the above error will be returned. Hope the question can be answered. Thanks!