From eee1d0a1424948fb6767e60e12ed1ea1f255a5fe Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Thu, 3 Jan 2019 23:48:54 +0100
Subject: [PATCH] smtbmc error test case 2

---
 vai_reg/symbiyosys.sby | 4 ++--
 vai_reg/vai_reg.vhd    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/vai_reg/symbiyosys.sby b/vai_reg/symbiyosys.sby
index 03b5552..67f9153 100644
--- a/vai_reg/symbiyosys.sby
+++ b/vai_reg/symbiyosys.sby
@@ -6,8 +6,8 @@ mode prove
 #mode cover
 
 [engines]
-#smtbmc
-abc pdr
+smtbmc
+#abc pdr
 
 [script]
 verific -vhdl vai_reg.vhd
diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd
index ffa71c4..94b0b8e 100644
--- a/vai_reg/vai_reg.vhd
+++ b/vai_reg/vai_reg.vhd
@@ -111,10 +111,10 @@ begin
             if (DinStop_i = '1') then
               if (unsigned(a_addr) <= 7) then
                 -- Following line results in a Segmentation Fault
-                --s_register(to_integer(unsigned(a_addr))) <= Din_i;
+                s_register(to_integer(unsigned(a_addr))) <= Din_i;
                 -- Following line results in following error:
                 -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172.
-                s_register(0) <= Din_i;
+                --s_register(0) <= Din_i;
               else
                 s_error <= true;
               end if;