#!/bin/sh

echo
echo Running ABC...
echo

$SMV_DIR/lib/smv/aigtoaig $1 ${1/.aag/.aig}

if ($SMV_DIR/lib/smv/abc -c "dprove; write_counter $2" ${1/.aag/.aig} | tee abc.log)
then
  echo 
  echo ABC terminated normally
  echo
  if grep -q "Networks are not equivalent" abc.log
  then
     echo
     echo Property falsified
     echo
     rm abc.log
     exit 0
  else
    if grep -q "Networks are equivalent" abc.log
    then
     echo
     echo Property proved
     echo
     echo t > $2
     rm abc.log
     exit 0
    fi
  fi
  echo
  echo No result
  echo
  rm -f $2
  touch $2
  rm abc.log
  exit 0
else
  echo 
  echo ABC terminated abnormally
  echo
  rm abc.log
  exit 1
fi
      
     


