We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Hi, for the following formula
(set-logic QF_NIA) (declare-fun i2 () Int) (assert (= true true true true (distinct 0 (abs i2) 3337))) (check-sat)
yices_smt2 --incremental yields
yices_smt2 --incremental
(error "mcsat: unsupported theory")
After replacing abs i2 with i2, yices can work well. Is this because of a missing support of the abs function?
abs i2
i2
abs
The text was updated successfully, but these errors were encountered:
7958d99
dddejan
No branches or pull requests
Hi, for the following formula
yices_smt2 --incremental
yieldsAfter replacing
abs i2
withi2
, yices can work well.Is this because of a missing support of the
abs
function?The text was updated successfully, but these errors were encountered: