SMTChecker: Malformed SMT-LIB2 script generated

[blishko]

On the following file, SMTChecker generates invalid SMT-LIB2 script if run with the options --model-checker-engine all --model-checker-solvers smtlib2 --model-checker-print-query --model-checker-ext-calls trusted.

contract D {
    function zero() public view returns (uint)  {
        return 0;
    }
}

contract C {
    uint x;
    function f(D d) public view {
        uint res = d.zero();
        assert(x < 1000);
    }

    function inc() public {
        ++x;
    }
}

This is the generated SMT-LIB script:

(set-option :produce-models true)
(set-logic ALL)
(declare-fun |_3_6| () Int)
(declare-fun |x_11_3| () Int)
(declare-fun |d_14_3| () Int)
(declare-fun |res_18_3| () Int)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|storage_C_38_type| 0)) (((|storage_C_38_type| (|x_11_C_38| Int)))))
(declare-datatypes ((|storage_type| 0)) (((|storage_type| (|storage_C_38| (Array Int |storage_C_38_type|))))))
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)) (|isActive| (Array Int Bool)) (|storage| |storage_type|)))))
(declare-fun |state_0| () |state_type|)
(declare-fun |_3_7| () Int)
(declare-fun |x_11_4| () Int)
(declare-fun |d_14_4| () Int)
(declare-fun |res_18_4| () Int)
(declare-fun |_3_0| () Int)
(declare-fun |x_11_5| () Int)
(declare-fun |expr_5_0| () Int)
(declare-fun |_3_1| () Int)
(declare-fun |_3_2| () Int)
(declare-fun |x_11_6| () Int)
(declare-fun |d_14_5| () Int)
(declare-fun |res_18_5| () Int)
(declare-fun |_3_3| () Int)
(declare-fun |x_11_7| () Int)
(declare-fun |d_14_6| () Int)
(declare-fun |res_18_6| () Int)
(declare-fun |x_11_0| () Int)
(declare-fun |d_14_0| () Int)
(declare-fun |res_18_0| () Int)
(declare-fun |x_11_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_20_abstract_1| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |x_11_2| () Int)
(declare-fun |fresh_balances_5_0| () (Array Int Int))
(declare-fun |state_1| () |state_type|)
(declare-fun |expr_21_0| () Int)
(declare-fun |res_18_1| () Int)
(declare-fun |expr_24_0| () Int)
(declare-fun |expr_25_0| () Int)
(declare-fun |expr_26_1| () Bool)

(assert
  (and
    (and
      (and true true)
      (and
        (= expr_26_1 (< expr_24_0 expr_25_0))
        (and
          (=> (and true true) true)
          (and
            (= expr_25_0 1000)
            (and
              (=>
                (and true true)
                (and
                  (>= expr_24_0 0)
                  (<=
                    expr_24_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
              (and
                (= expr_24_0 x_11_2)
                (and
                  (ite (and true true) (= res_18_1 expr_21_0) (= res_18_1 res_18_0))
                  (and
                    (= state_1 (|state_type| fresh_balances_5_0))
                    (and
                      (and
                        (>= x_11_2 0)
                        (<=
                          x_11_2
                          115792089237316195423570985008687907853269984665640564039457584007913129639935))
                      (and
                        (=> (and true true) true)
                        (and
                          (= expr_19_0 d_14_0)
                          (and
                            (= expr_20_abstract_1 1612685573)
                            (and
                              (and
                                (>= d_14_0 0)
                                (<= d_14_0 1461501637330902918203684832716283019655932542975))
                              (and
                                (= res_18_0 0)
                                (and
                                  (and
                                    (>= x_11_1 0)
                                    (<=
                                      x_11_1
                                      115792089237316195423570985008687907853269984665640564039457584007913129639935))
                                  (and
                                    (and
                                      (and
                                        (and
                                          (and
                                            (and
                                              (and
                                                (and
                                                  (and
                                                    (and
                                                      (and
                                                        (and
                                                          (and
                                                            (> (|block.prevrandao| tx_0) 18446744073709551616)
                                                            (and
                                                              (>= (|block.basefee| tx_0) 0)
                                                              (<=
                                                                (|block.basefee| tx_0)
                                                                115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                                          (and
                                                            (>= (|block.chainid| tx_0) 0)
                                                            (<=
                                                              (|block.chainid| tx_0)
                                                              115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                                        (and
                                                          (>= (|block.coinbase| tx_0) 0)
                                                          (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)))
                                                      (and
                                                        (>= (|block.prevrandao| tx_0) 0)
                                                        (<=
                                                          (|block.prevrandao| tx_0)
                                                          115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                                    (and
                                                      (>= (|block.gaslimit| tx_0) 0)
                                                      (<=
                                                        (|block.gaslimit| tx_0)
                                                        115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                                  (and
                                                    (>= (|block.number| tx_0) 0)
                                                    (<=
                                                      (|block.number| tx_0)
                                                      115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                                (and
                                                  (>= (|block.timestamp| tx_0) 0)
                                                  (<=
                                                    (|block.timestamp| tx_0)
                                                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                              (and
                                                (>= (|msg.sender| tx_0) 0)
                                                (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975)))
                                            (and
                                              (>= (|msg.value| tx_0) 0)
                                              (<=
                                                (|msg.value| tx_0)
                                                115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                          (and
                                            (>= (|tx.origin| tx_0) 0)
                                            (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975)))
                                        (and
                                          (>= (|tx.gasprice| tx_0) 0)
                                          (<=
                                            (|tx.gasprice| tx_0)
                                            115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                                      (and
                                        (and
                                          (and
                                            (and
                                              (and
                                                (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 4234695194))
                                                (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 252))
                                              (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 104))
                                            (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 82))
                                          (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 26))
                                        (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)))
                                    true))))))))))))))))
    (not expr_26_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| _3_3))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_11_2))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| d_14_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| res_18_1))
(check-sat)

The problem with the script is with the state_type data type. It is declared with three members, but then applied to a single field in the body of the query.

[blishko]

The problem seems to be with the symbolic variable for the blockchain state, which has different type in CHC engine and in BMC engine, if trusted mode is used to analyze external calls.