#!/bin/sh
# the next line restarts using tclsh \
exec tclsh "$0" "$@"

set f [open "|ztrace [lindex $argv 0]" "r"]
set outfile [open [lindex $argv 1] "w"]

while {![eof $f]} {
    gets $f l
    puts $l
    if {[string match *unsatisfiable* $l]} {
	puts $outfile 0
    } elseif {[string match *satisfiable* $l]} {
	puts $outfile 1
	while {![eof $f]} {
	    gets $f l
	    if {[string match Max* $l]} {
		break
	    }
	    puts $outfile $l
	}
    }
}

close $f
close $outfile
