[SMTChecker] Refactor counterexamples to parse smtlib2 instead of APIs
Open
must have eventually
smt
- Dominant language
- C++
- Stars
- 25.7k
- Forks
- 6.2k
- Avg merge
- 2d 19h
- Merged PRs (30d)
- 29
Description
The general goal is to remove the solver APIs (z3 and cvc4). We need to be able to do everything using the smtlib2 interface. Currently this already works for solving but not for counterexamples and invariants.
Contributor guide
Assessment
This issue has not been assessed yet.