Frank Busse
Frank Busse
> I've been tuning STP to solve difficult problems faster, not to solve easy problems faster. [...] Does anyone have problems that they'd like the next release to not be...
I ran a single(!) experiment with different STP versions / SAT solvers. Below are 1h KLEE runs with DFS search heuristic - that means the queries are typically easier to...
Just checked, three cases are crashes (maybe an API change?), e.g.: ``` error: STP Error: SimplifyAtomicFormula: NO atomic formula of the kind ``` ``` error: STP Error: TransformArray: An array...
Let me try to log the queries for the crashing cases.
I looked at `nl` as outlier - one of the queries that seem to run longer on my machine with STP master is attached (.kquery and .smt2). ``` > kleaver...
> Could it be that case that reading from the counter example is really slow? Maybe but why? > You're doing this via the C-api right? Yes: https://github.com/klee/klee/blob/c9de012b07426435b8bd3bb29082fbceddf403a3/lib/Solver/STPSolver.cpp#L201
From the KLEE side: CryptoMinisat in the past has been really slow in comparison to MiniSat for my benchmarks and I refrained from using it. However, I did a quick...
> STP requires 1 or more modern SAT solver to link to (i.e. CMS, Cadical or Riss). Why would you make it a requirement and not just a warning (during...
> "Use version x.yy if you absolutely need MiniSat. This version is deprecated, and support requests may be unanswered." This is bad from a user's perspective. STP is packaged typically...
While doing so keep in mind #512. ;)