leonardoalt

// Check whether `model` evaluates `phi` to true.
// `phi` must be in 3-CNF.
// The length of `model` is the max number of distinct variables in the formula.
// The length of `phi` is the max number of clauses in the formula.
// A literal `x` in `phi` represents variable `x / 2` with positive polarity if
// `x` is even, and negative polarity if `x` is odd.

struct Clause {
	u32[3] literals
}

leonardoalt

struct Stack {
	u32[21] values
	u32 length
}

struct Memory {
	u32[16] values
}

struct State {

leonardoalt

(set-logic HORN)

(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int 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.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-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-datatypes ((|t_function_abiencodepacked_pure()returns(t_bytes_memory_ptr)_t_bytes3

leonardoalt

(set-logic HORN)

(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int 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.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-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-datatypes ((|t_function_abiencodepacked_pure()returns(t_bytes_memory_ptr)_t_bytes3

leonardoalt

(set-logic HORN)

(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int 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.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-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-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-datatypes ((|mapping(uint256

leonardoalt

interface Token {
	function balanceOf(address _a) external view returns (uint);
	function transfer(address _to, uint _amt) external;
}

contract TokenCorrect is Token {
	mapping (address => uint) balance;
	constructor(address _a, uint _b) {
		balance[_a] = _b;
	}

leonardoalt

(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.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_45_1 () Bool)
(declare-fun tx_0 () tx_type)
(declare-fun r_33_0 () Int)
(declare-fun x_3_0 () Int)
(declare-fun y_5_0 () Int)
(declare-fun k_7_0 () Int)
(declare-fun expr_11_0 () Int)
(declare-fun expr_12_0 () Int)

leonardoalt

(declare-datatypes ((ecrecover_input_type 0)) (((ecrecover_input_type (hash Int) (v Int) (r Int) (s Int)))))
(declare-datatypes ((storage_State_42_type 0)) (((storage_State_42_type (x_20_State_42 Int) (o_23_State_42 Int) (c_26_State_42 Int)))))
(declare-datatypes ((storage_Other_18_type 0)) (((storage_Other_18_type (c_4_Other_18 Int)))))
(declare-datatypes ((storage_C_103_type 0)) (((storage_C_103_type (owner_44_C_103 Int) (y_46_C_103 Int) (s_49_C_103 Int)))))
(declare-datatypes ((storage_type 0)) (((storage_type (storage_C_103 (Array Int storage_C_103_type)) (storage_Other_18 (Array Int storage_Other_18_type)) (storage_State_42 (Array Int storage_State_42_type))))))
(declare-datatypes ((abi_type 0)) (((abi_type))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int)) (isActive (Array Int Bool)) (storage storage_type)))))
(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)

leonardoalt

(declare-datatypes ((ecrecover_input_type 0)) (((ecrecover_input_type (hash Int) (v Int) (r Int) (s Int)))))
(declare-datatypes ((abi_type 0)) (((abi_type))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int 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.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-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-rel block_7_exp_38_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel contract

leonardoalt

sat
(let ((a!1 (forall ((A Int)
                    (B abi_type)
                    (C crypto_type)
                    (D tx_type)
                    (E state_type))
             (! (=> (and (>= (tx.origin D) 0)
                         (>= (tx.gasprice D) 0)
                         (>= (msg.value D) 0)
                         (>= (msg.sender D) 0)