Mikhail R. Gadelha
Mikhail R. Gadelha
> Why don't spend the time and effort implementing the new feature following > the current design? > > This is an open-source project. People spend their time and effort...
> (1) the reviewer will implement his/her comment and/or (2) another > reviewer will make the final decision. > > These are unreasonable. So the choices are to either give...
It was handled internally before, but there was problems whenever SV-COMP decides to change the function definition. Em qua., 1 de jun. de 2022 às 13:30, Rafael Sá Menezes <...
ping. Any updates on releasing a new version?
> > Running ESBMC with Boolector takes a few seconds to prove while Z3 times out after 5min. However, exporting the formula generated by boolector and feeding it to Z3...
the incompatible ones happen because of data types: we replace it with our implementation of data types with the flags tuple-node and tuple-sym. The z3 configuration I've mentioned was https://github.com/esbmc/esbmc/blob/master/src/solvers/z3/z3_conv.cpp#L54-L62,...
> Even so, running the same formula with the solver binaries gave the same result. z3 probably needs to be better configured to your needs
nice Em qua., 21 de fev. de 2024 às 17:13, Rafael Sá Menezes < ***@***.***> escreveu: > Update: z3 team just merged a patch that should fix this issue. >...
Is the slowdown in ESBMC or the SMT solver? If the latter, we can try to use the array flattener and check if we get any improvements. Em sex., 23...
> > Should we consider evolving the format? > Definitely; having to duplicate test cases to test them with different flags is a major drawback IMHO — also perl. I...