Merge pull request #236 from diffblue/two-tests-now-work

two 'eventually' tests now work

Author: tautschnig

regression/ebmc/SVA-LTL/lasso1-counterexample.desc

@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 lasso1.sv
---bound 10 --trace
+--bound 10 --waveform
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[top\.property\.p0\] .* FAILURE$
+^             0  1  2  3  4  5  6  7  8  9 10$
+^top\.counter  0  1  2  3  4  5  6  7  8  9  3$
 --
 --
-The reported counterexample should be longer, to include the loop.

regression/ebmc/SVA-LTL/lasso1-small-bound.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 lasso1.sv
 --bound 5
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[top\.property\.p0\] .* SUCCESS$
 --
 --
-The bound is too small to find the counterexample, and hence, SUCCESS should
-be reported.