* [spacer] logging solver events
New option fp.spacer.trace_file='file.log' enables logging solving events
into a file.
These events are useful for debugging the solver, but also for visualizing
the solving process in a variety of ways
* [spacer] allow setting logic for solvers used by spacer
* [spacer] option to set arithmetic solver explicitly
* [spacer] improve of dumping solver_pool state for debugging
* fix propagate_ineqs to handle strict inequality
Co-authored-by: Nham Van Le <nv3le@precious3.eng.uwaterloo.ca>
Background external invariants are constraints that are assumed to be
true of the system. This commit introduces a mode in which
background invariants are used only duing inductive generalization
and lemma pushing, but not during predecessor computation.
It is believed that this will be more efficient used of background
external invariants since they will not be able to disturb how
predecessors are generalized and computed.
Based on a patch by Jorge Navas
