Lines Matching refs:vc
34 VC vc = vc_createValidityChecker(); in TEST() local
37 Type bv32 = vc_bvType(vc, 32); in TEST()
44 Expr n = vc_varExpr(vc, "n", bv32); in TEST()
47 Expr v = vc_varExpr(vc, "v", bv32); in TEST()
48 Expr ct_4 = vc_bvConstExprFromInt(vc, 32, 4); in TEST()
49 Expr add_v_4 = vc_bvPlusExpr(vc, 32, v, ct_4); in TEST()
56 Expr ge = vc_bvGeExpr(vc, add_v_4, v); in TEST()
60 vc_push(vc); in TEST()
64 Expr f_add = vc_eqExpr(vc, add_v_4, n); in TEST()
65 vc_assertFormula(vc, f_add); in TEST()
66 vc_printExpr(vc, f_add); in TEST()
71 vc_assertFormula(vc, ge); in TEST()
72 vc_printExpr(vc, ge); in TEST()
77 Expr f_numeq = vc_eqExpr(vc, ct_4, n); in TEST()
78 vc_assertFormula(vc, f_numeq); in TEST()
79 vc_printExpr(vc, f_numeq); in TEST()
84 vc_printAsserts(vc); in TEST()
86 int query = vc_query(vc, vc_falseExpr(vc)); in TEST()
91 vc_pop(vc); in TEST()