Etienne Kneuss
authored
- Choose expressions becomes uninterpreted functions under the same constraints. - Fix bug with variablesOf considering choose binders as free. - Silence evaluator errors when occuring with tentative lucky models. Note that choose expressions cannot be evaluated nor compiled.
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| z3 | ||
| IncrementalSolver.scala | ||
| InterruptibleSolver.scala | ||
| ParallelSolver.scala | ||
| RandomSolver.scala | ||
| Solver.scala | ||
| TimeoutSolver.scala | ||
| TrivialSolver.scala | ||