Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
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
Merged horn_traces branch