kdrag.contrib.fast.test

kdrag.contrib.fast.test()

>>> myadd(2, 3)
5
>>> ctx = ffibuilder.cast("void *", z3.main_ctx().ctx.value)
>>> ast = my_mk_true(ctx)
>>> value = intify(ast)
>>> z3.BoolRef(value)
True
>>> z3.BoolRef(intify(my_mk_and(ctx, ast, ast)))
And(True, True)
>>> z3.AstVector(intify(KDRAG_get_consts(ctx, ast)), z3.main_ctx())
[True]
>>> x = z3.Int("x")
>>> z3.AstVector(intify(KDRAG_get_consts(ctx, astptr(x + x + x))), z3.main_ctx())
[x]