Internal Yices Bug

[ekiwi]

Hi, sorry for opening another issue. I was trying to play around with options for implementing constant array initialization with yices and ended up with an input that leads to the following message from yices:

(error "BUG detected")

*************************************************************
FATAL ERROR: smt2_commands
*************************************************************
Please report this bug to yices-bugs@csl.sri.com.
To help us diagnose this problem, please include the
following information in your bug report:

  Yices version: 2.6.4
  Build date: 2022-07-09
  Platform: x86_64-pc-linux-gnu (release)

Thank you for your help.
*************************************************************

Here is the SMT file content:

(set-logic QF_AUFBV)
(declare-sort OutOfBoundsValueIs_s 0)
(declare-fun reset_f (OutOfBoundsValueIs_s) Bool)
(declare-fun readAddr_f (OutOfBoundsValueIs_s) (_ BitVec 2))
(declare-fun m_out_MPORT_rand_data_f (OutOfBoundsValueIs_s) (_ BitVec 8))
(declare-fun m_f (OutOfBoundsValueIs_s) (Array (_ BitVec 2) (_ BitVec 8)))
(declare-fun _resetCount_f (OutOfBoundsValueIs_s) Bool)
(define-fun m.out_MPORT.addr_f ((state OutOfBoundsValueIs_s)) (_ BitVec 2) (readAddr_f state))
(define-fun m.out_MPORT.data_f ((state OutOfBoundsValueIs_s)) (_ BitVec 8) (select (m_f state) (m.out_MPORT.addr_f state)))
(define-fun m_out_MPORT_addr_f ((state OutOfBoundsValueIs_s)) (_ BitVec 2) (readAddr_f state))
(define-fun m_out_MPORT_oob_f ((state OutOfBoundsValueIs_s)) Bool (not (bvugt (_ bv3 2) (m_out_MPORT_addr_f state))))
(define-fun m_out_MPORT_rand_data.en_f ((state OutOfBoundsValueIs_s)) Bool (m_out_MPORT_oob_f state))
(define-fun _T_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv0 2)))
(define-fun out_f ((state OutOfBoundsValueIs_s)) (_ BitVec 8) (ite (m_out_MPORT_oob_f state) (m_out_MPORT_rand_data_f state) (m.out_MPORT.data_f state)))
(define-fun _T_1_f ((state OutOfBoundsValueIs_s)) Bool (= (out_f state) (_ bv0 8)))
(define-fun _T_3_f ((state OutOfBoundsValueIs_s)) Bool (not (reset_f state)))
(define-fun _T_4_f ((state OutOfBoundsValueIs_s)) Bool (not (_T_1_f state)))
(define-fun _T_5_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv1 2)))
(define-fun _T_10_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv2 2)))
(define-fun _T_15_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv3 2)))
(define-fun _resetPhase_f ((state OutOfBoundsValueIs_s)) Bool (not (bvuge (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assert_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_1_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_5_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_2_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_10_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_3_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_15_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun _resetActive_f ((state OutOfBoundsValueIs_s)) Bool (=> (_resetPhase_f state) (reset_f state)))
(define-fun m.out_MPORT.en_f ((state OutOfBoundsValueIs_s)) Bool true)
(define-fun m_next ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) (m_f state))
(define-fun const_array_0 ((index (_ BitVec 2))) (_ BitVec 8) (_ bv0 8))
(define-fun m_init ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) const_array_0)
(define-fun _resetCount_next ((state OutOfBoundsValueIs_s)) Bool (ite (_resetPhase_f state) (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) (_resetCount_f state)))
(define-fun _resetCount_init ((state OutOfBoundsValueIs_s)) Bool false)
(define-fun OutOfBoundsValueIs_t ((state OutOfBoundsValueIs_s) (state_n OutOfBoundsValueIs_s)) Bool (and (= (m_f state_n) (m_next state)) (= (_resetCount_f state_n) (_resetCount_next state))))
(define-fun OutOfBoundsValueIs_i ((state OutOfBoundsValueIs_s)) Bool (and (= (m_f state) (m_init state)) (= (_resetCount_f state) (_resetCount_init state))))
(define-fun OutOfBoundsValueIs_a ((state OutOfBoundsValueIs_s)) Bool (and (assert_f state) (and (assert_1_f state) (and (assert_2_f state) (assert_3_f state)))))
(define-fun OutOfBoundsValueIs_u ((state OutOfBoundsValueIs_s)) Bool (_resetActive_f state))
(declare-fun s0 () OutOfBoundsValueIs_s)
(assert (OutOfBoundsValueIs_i s0))
(assert (_resetActive_f s0))
(assert (not (and (assert_f s0) (and (assert_1_f s0) (and (assert_2_f s0) (assert_3_f s0))))))
(check-sat)

My attempt to create an array initialized to a constant (replacing the non-standard as const) consists of these two lines:

(define-fun const_array_0 ((index (_ BitVec 2))) (_ BitVec 8) (_ bv0 8))
(define-fun m_init ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) const_array_0)

which originally were:

(define-fun m_init ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) (_ bv0 8)))

Btw, in case you are curious: All if this is part of an effort to add yices2 support to the chiseltest bounded model checking backend

Best, Kevin