#!/bin/bash     

#Each file should be simplified down to either true or false, so the CNF generated should
#be very small if simplifications are working as they should.

rm -f output_*.cnf

files=`ls -1 -S *.smt2`
for f in $files; do
	stp --simplifying-minisat --output-CNF $f
	cnf=`cat output_*.cnf  | wc -l`
	if [ $cnf -gt 3 ] ; then
		echo --fail
		exit 10
	fi

done


#!/bin/bash     

#Each file should be simplified down to either true or false, so the CNF generated should
#be very small if simplifications are working as they should.

rm -f output_*.cnf

files=`ls -1 -S *.smt2`
for f in $files; do
	stp --output-CNF $f
	cnf=`cat output_*.cnf  | grep -v "^c" | grep -v "^$" |  wc -l`
	if [ $cnf -gt 3 ] ; then
		echo --fail
		exit 10
	fi

done


Fix the unit test script: * To not explicitly call simplifying minisat (which isn't an option if compiled with cms). * To remove comments and blank lines (which are introduced by AIG's conversion).
Fix the unit test script:
* To not explicitly call simplifying minisat (which isn't an option if compiled with cms).
* To remove comments and blank lines (which are introduced by AIG's conversion).



git-svn-id: 5069ba8be4c997ee907bf46f8ec9a2bbfb655637@937 e59a4935-1847-0410-ae03-e826735625c1
