diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index b816e84b8..fb1a16b15 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -99,6 +99,7 @@ namespace smt { bool get_upper(enode* n, rational& r, bool& is_strict); void solve_for(vector& s) override; + // check if supplied set of linear constraints are LP feasible within current backtracking context // identify core by setting Boolean flags to true for constraints used in the proof of infeasibility // and return l_false if infeasible.