Skip to content
New issue

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

Assertion violation at smtrat-modules/SATModule/SATModule.cpp:389 (mcsat) #71

Closed
rainoftime opened this issue May 2, 2020 · 1 comment
Labels
invalid meaningless See, e.g., https://github.com/Z3Prover/z3/issues/4461#issuecomment-633988515 wontfix

Comments

@rainoftime
Copy link

Hi, for the following formula,

(set-logic QF_NIA)
(declare-fun _substvar_12_ () Int)
(assert (>= 802 _substvar_12_))
(check-sat)
(check-sat)

smtrat (commit 97e3c34) throws an assertion violation

sat
smtrat-static: /home/peisen/test/smtrat-asan/src/smtrat-modules/SATModule/SATModule.cpp:389: smtrat::Answer smtrat::SATModule<Settings>::checkCore() [with Settings = smtrat::SATSettingsMCSATOC]: Assertion `mMCSAT.level() == 0' failed.

Build configuration:

set(SMTRAT_Strategy "MCSATOC" CACHE STRING "Used strategy in the solver")
@nafur
Copy link
Contributor

nafur commented May 27, 2020

Please stop submitting issues if you don't know what you are doing. Our MCSAT does not support integers.

@nafur nafur added invalid meaningless See, e.g., https://github.com/Z3Prover/z3/issues/4461#issuecomment-633988515 wontfix labels May 27, 2020
@nafur nafur closed this as completed May 27, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
invalid meaningless See, e.g., https://github.com/Z3Prover/z3/issues/4461#issuecomment-633988515 wontfix
Projects
None yet
Development

No branches or pull requests

2 participants