Remove `lia_generic`
This rule is a legacy macro rule. It is hard to reconstruct and essentially needs an integer solver to be reconstructed.
In veriT this rule is generated by LA_xx_conflict_proof_z
in src/arith/LA-xx.c.tpl
which is only called if LA_solve_z
returns the status UNSAT. LA_solve_z
is a simple search for integer solutions with bounds.
Instead of having one lia_generic
step for all of this we should have multiple la_generic steps for the bounds and then resolutions for the final clause which is currently produced by lia_generic
.
We should also check how this is handled in CVC4.