graph-refine: fix order of evaluation for saving SMT proof check

graph-refine: fix string type bug

graph-refine: make behavior easier to emulate

graph-refine: don't use json for proof checks dump

graph-refine: don't use json for proof checks dump

graph-refine: add feature for saving smt proof checks

graph-refine: use correct method name

graph-refine: add feature for loading inline scripts

graph-refine: broaden search for loop match

Before this change, loop_no_match failed to recognize the correspondence
between a C loop in create_untypeds and its optimized ASM.

The loop had a constant number of iterations
(ARRAY_SIZE(ndks_boot.freemem) = 4), and the optimized version counted
down rather than up.

graph-refine: broaden search for loop match

Before this change, loop_no_match failed to recognize the correspondence
between a C loop in create_untypeds and its optimized ASM.

The loop had a constant number of iterations
(ARRAY_SIZE(ndks_boot.freemem) = 4), and the optimized version counted
down rather than up.