use the test.pl script from the CBMC repo

This removes the test.pl script from this repo, and runs the one from the
CBMC dependency instead.

Author: kroening

regression/ebmc/BDD1/test.desc

@@ -3,6 +3,6 @@ main.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[smv::main::spec1\] AG (!main::var::some_var = off): SUCCESS$
+^\[smv::main::spec1\] AG \(!main::var::some_var = off\): SUCCESS$
 --
 ^warning: ignoring

regression/ebmc/Makefile

@@ -1,17 +1,4 @@
-default: tests.log
-
-include ../../lib/cbmc/src/config.inc
-include ../../lib/cbmc/src/common
+default: test
 
 test:
-	@../test.pl -c ../../../src/ebmc/ebmc
-
-tests.log: ../test.pl
-	@../test.pl
-
-show:
-	@for dir in *; do \
-		if [ -d "$$dir" ]; then \
-			vim -o "$$dir/main.c" "$$dir/main.out"; \
-		fi; \
-	done;
+	@../../lib/cbmc/regression/test.pl -c ../../../src/ebmc/ebmc

regression/ebmc/range_type4/test.desc

@@ -3,6 +3,6 @@ main.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[smv::main::spec1\] AG (!main::var::x = 6): SUCCESS$
+^\[smv::main::spec1\] AG \(!main::var::x = 6\): SUCCESS$
 --
 ^warning: ignoring

regression/ebmc/range_type5/test.desc

@@ -3,6 +3,6 @@ main.smv
 --bound 3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[smv::main::spec1\] AG (!main::var::x = 6): SUCCESS$
+^\[smv::main::spec1\] AG \(!main::var::x = 6\): SUCCESS$
 --
 ^warning: ignoring

regression/test.pl

@@ -1,14 +1,4 @@
-default: tests.log
+default: test
 
 test:
-	@../test.pl -c ../../../src/ebmc/ebmc
-
-tests.log: ../test.pl ../../../src/ebmc/ebmc
-	@../test.pl
-
-show:
-	@for dir in *; do \
-		if [ -d "$$dir" ]; then \
-			vim -o "$$dir/main.c" "$$dir/main.out"; \
-		fi; \
-	done;
+	@../../lib/cbmc/regression/test.pl -c ../../../src/ebmc/ebmc