Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

test/test-compile.sh
151 151
    else
152 152
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
153 153
    fi
154
    if [ $? -ne 0 ]; then
155
        rlustrec="INVALID";
156
    else
157
        rlustrec="VALID"
158
    fi
154 159
    # echo "z3 $build/$name".smt2 
155 160
    # TODO: This part of the script has to be optimized
156 161
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
......
160 165
        rhorn="VALID"
161 166
    fi
162 167
    if [ $verbose -gt 0 ]; then
163
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
168
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
164 169
    else
165
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
170
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
166 171
    fi
167 172
    popd > /dev/null
168 173
done < $file_list

Also available in: Unified diff