issues
search
ufmg-smite
/
lean-smt
Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
94
stars
19
forks
source link
Usability improvements
#38
Closed
Vtec234
closed
2 years ago
Vtec234
commented
2 years ago
Add
smt_show
tactic which just shows the query but does not run a solver.
Support setting a solving timeout.
Default to a 5s timeout since it is too easy for unsuspecting users to blow up their machine with a heavy query.
smt_showtactic which just shows the query but does not run a solver.