add tests for SMV LTLSPEC

regression/ebmc/smv/smv_ltlspec_F3.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+smv_ltlspec_F3.smv
+--bound 10
+^\[.*\] F x = 0: REFUTED$
+^Counterexample with 4 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^x@3 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_F3.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3, 3, ...
+LTLSPEC F x = 0

regression/ebmc/smv/smv_ltlspec_G3.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+smv_ltlspec_G3.smv
+--bound 10
+^\[.*\] G X x != 3: REFUTED$
+^Counterexample with 3 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G3.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+LTLSPEC G X x!=3

regression/ebmc/smv/smv_ltlspec_R2.desc

@@ -0,0 +1,14 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_R2.smv
+--bound 10
+^\[.*\] FALSE R x != 3: REFUTED$
+^Counterexample with 4 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The trace has too many states.

regression/ebmc/smv/smv_ltlspec_R2.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+LTLSPEC FALSE R x != 3

regression/ebmc/smv/smv_ltlspec_R3.desc

@@ -0,0 +1,10 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_R3.smv
+--bound 1
+^\[.*\] FALSE R x != 3: PROVED up to bound 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The counterexample is wrong.

regression/ebmc/smv/smv_ltlspec_R3.smv

@@ -0,0 +1,16 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+-- hence no trace with k=1
+LTLSPEC FALSE R x != 3

regression/ebmc/smv/smv_ltlspec_R4.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+smv_ltlspec_R4.smv
+--bound 10
+^\[.*\] FALSE R x != 0: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/smv/smv_ltlspec_R4.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- should pass
+LTLSPEC FALSE R x != 0

regression/ebmc/smv/smv_ltlspec_U2.desc

@@ -0,0 +1,15 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_U2.smv
+--bound 10
+^\[.*\] TRUE U x = 0: REFUTED$
+^Counterexample with 4 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^x@3 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The property is proven, but should be refuted.

regression/ebmc/smv/smv_ltlspec_U2.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3, 3, ...
+LTLSPEC TRUE U x = 0