#!/usr/bin/gawk -f
BEGIN{
	bees="";
}

/^[ ]+\(define-fun.*Int$/{
	bees = $2;
}

/^[ ]+[0-9]+\)/{
	match ($0, /^[ ]+([0-9]+)\)/, arr)
	print bees " " arr[1];
}

Add parser for Z3's get-model output.

Doesn't really parse it, it just reformats it into something less
rubbish.
