Lines Matching refs:pre
14 // express some assertions with some pre-conditions.
199 static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
204 BoolectorNode *p = boolector_and(btor, *pre, n);
205 *pre = p;
233 static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
238 return check_btor(btor, pre, n, insn);
241 static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
246 return check_btor(btor, pre, n, insn);
265 static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
271 return add_precondition(btor, pre, insn);
273 return check_assert(btor, *pre, insn);
275 return check_equal(btor, *pre, insn);
284 BoolectorNode *pre = boolector_true(btor);
312 rc &= check_call(btor, &pre, insn);