Merge pull request #816 from diffblue/BMC-AX1

BMC: KNOWNBUG test for AXp

Author: tautschnig

regression/ebmc/BMC/AX1.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+AX1.smv
+--bound 2
+^\[spec1\] AX some_var = TRUE: REFUTED$
+^\[spec2\] AX some_var = FALSE: PROVED up to bound 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC encoding fails on the temporal operator.

regression/ebmc/BMC/AX1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = FALSE
+
+-- should fail
+SPEC AX some_var = TRUE
+
+-- should pass
+SPEC AX some_var = FALSE