Is there any case that z3 reports 'unsat' when logic is insufficient? #6282
Answered
by
NikolajBjorner
kangwoosukeq
asked this question in
Q&A
-
|
According to #3916, there is a case that z3 reports 'sat' when given logic doesn't cover some components of the expression. Then, I want to ask if there is any possible case that z3 reports 'unsat' when a part of the expression is expressed uninterpreted because of its logic. |
Beta Was this translation helpful? Give feedback.
Answered by
NikolajBjorner
Aug 18, 2022
Replies: 1 comment
-
|
no |
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
kangwoosukeq
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
no