mcBV returns false answer

[mm95]

Hi,
I have a case study and run it with mcBV.exe .
This formula is sat in checking with z3, but in mcBV, after about 4000 second, I recieve unsat or exactly below message.
" Z3> Error, literal in conflict clause is not false (-440=True)
unsat
4347.132141 sec"
binsearch.smt2.txt

[wintersteiger]

That's definitely a bug, thanks for reporting this!

[mm95]

You're welcome. May I am hopeful that it is resolved soon?

…

On Thu, Mar 2, 2017 at 2:26 PM, Christoph M. Wintersteiger < ***@***.***> wrote: That's definitely a bug, thanks for reporting this! — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#3 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AWTNR0SIwZ_6wlalxNKRdZXrzxuSBsu9ks5rhqBAgaJpZM4MQqEL> .

[wintersteiger]

I'm fairly sure that this will take a significant amount of time. It's not a bug that we have a short/simple/quick test file for and I'm currently super busy with unrelated projects.

[mm95]

Ok. Thanks so much.

…

On Thu, Mar 2, 2017 at 2:47 PM, Christoph M. Wintersteiger < ***@***.***> wrote: I'm fairly sure that this will take a significant amount of time. It's not a bug that we have a short/simple/quick test file for and I'm currently super busy with unrelated projects. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#3 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AWTNR4-fIlII44xXzLIOgH_wxHLCbGXwks5rhqVSgaJpZM4MQqEL> .