Instructions to see raw SMTLib queries generated by SMTChecker from solc

Readme.md

Compile solc locally after applying the below patch (solc.patch).Build instructions.

./solc example.sol --model-checker-engine bmc

Call to check. Solver state:
(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.difficulty Int) (block.gaslimit Int) (block.number 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 expr_8_1 () Bool)
(declare-fun tx_0 () tx_type)
(declare-fun x_2_0 () Int)
(declare-fun expr_6_0 () Int)
(declare-fun expr_7_0 () Int)
(assert (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 0) 179))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 1) 222))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 2) 100))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 3) 139)))
  (and (and true true)
       (= expr_8_1 (> expr_6_0 expr_7_0))
       (=> (and true true) true)
       (= expr_7_0 5)
       (=> (and true true)
           (and (>= expr_6_0 0)
                (<= expr_6_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_6_0 x_2_0)
       (>= x_2_0 0)
       (<= x_2_0
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.basefee tx_0) 0)
       (<= (block.basefee tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.chainid tx_0) 0)
       (<= (block.chainid tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.coinbase tx_0) 0)
       (<= (block.coinbase tx_0)
           1461501637330902918203684832716283019655932542975)
       (>= (block.difficulty tx_0) 0)
       (<= (block.difficulty tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.gaslimit tx_0) 0)
       (<= (block.gaslimit tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.number tx_0) 0)
       (<= (block.number tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.timestamp tx_0) 0)
       (<= (block.timestamp tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (msg.sender tx_0) 0)
       (<= (msg.sender tx_0) 1461501637330902918203684832716283019655932542975)
       (>= (msg.value tx_0) 0)
       (<= (msg.value tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (tx.origin tx_0) 0)
       (<= (tx.origin tx_0) 1461501637330902918203684832716283019655932542975)
       (>= (tx.gasprice tx_0) 0)
       (<= (tx.gasprice tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (= (msg.value tx_0) 0)
       (= (msg.sig tx_0) 3017696395)
       a!1
       a!2
       a!3
       a!4
       (>= (bytes_tuple_accessor_length (msg.data tx_0)) 4)
       true
       (not expr_8_1))))

Warning: This is a pre-release compiler version, please do not use it in production.

Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> /tmp/test.sol

Warning: Source file does not specify required compiler version!
--> /tmp/test.sol

Warning: BMC: Assertion violation happens here.
 --> /tmp/test.sol:4:9:
  |
4 |         assert(x > 5);
  |         ^^^^^^^^^^^^^
Note: Counterexample:
  x = 0

Note: Callstack:
Note:

example.sol

contract C {
    function f(uint x) external pure {
        // Should fail
        assert(x > 5);
    }
}

solc.patch

diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 4abeffa16..69db6ac69 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -99,6 +99,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 {
 	CheckResult result;
 	vector<string> values;
+	std::cout << "Call to check. Solver state:\n" << m_solver << std::endl;
 	try
 	{
 		switch (m_solver.check())