Skip to content

Instantly share code, notes, and snippets.

@hrkrshnn
Last active April 4, 2023 08:11
Show Gist options
  • Save hrkrshnn/306ebb5fc4687062a6fd865451348137 to your computer and use it in GitHub Desktop.
Save hrkrshnn/306ebb5fc4687062a6fd865451348137 to your computer and use it in GitHub Desktop.
Instructions to see raw SMTLib queries generated by SMTChecker from solc

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:

contract C {
function f(uint x) external pure {
// Should fail
assert(x > 5);
}
}
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())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment