leonardoalt

; Horn encoding of the following pseudocode:
;
; assume x < y
; while (x < y) ++x;
; assert (x == y)
;
; We consider the CFG to be the following:
;
; Init -> LoopHeader
; LoopHeader -> LoopBody

leonardoalt

 (set-logic HORN)

(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-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$addressuint256$_tuple| 0)) (((|mapping$addressuint256$_tuple| (|mapping

leonardoalt

0x12a6ba34023bf553d8700b2b05737111a3cc19dd7842910e1f3b771278873f2e

leonardoalt

import * as fs from 'fs';
import * as path from 'path';

import solc from './';
import smtchecker from './smtchecker';
import smtsolver from './smtsolver';
          
const settings = { modelChecker: {
  contracts: {
    'a.sol': [ 'C' ]

leonardoalt

const fs = require('fs');
const path = require('path');

const solc = require('./index.js');
const smtchecker = require('./smtchecker.js');
const smtsolver = require('./smtsolver.js');
          
const settings = { modelChecker: {
  engine: 'chc',
  targets: ['assert'],

leonardoalt

(set-logic HORN)

(declare-fun |interface_0_C_19_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_19_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_19_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_19_0 error_0 this_0))))

leonardoalt

(set-logic HORN)

(declare-fun |interface_0_C_19_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_19_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_19_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_19_0 error_0 this_0))))

leonardoalt

(set-logic HORN)

(declare-fun |interface_0_C_33_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_33_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_33_0 error_0 this_0))))

leonardoalt

(set-logic HORN)

(declare-fun |interface_0_C_33_0| (Int ) Bool)
(declare-fun |nondet_interface_1_C_33_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_C_33_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_C_33_0 error_0 this_0))))

leonardoalt

(set-logic HORN)

(declare-fun |interface_0_I_4_0| (Int ) Bool)
(declare-fun |nondet_interface_1_I_4_0| (Int Int ) Bool)
(declare-fun |summary_constructor_2_I_4_0| (Int Int ) Bool)
(assert
(forall ( (error_0 Int) (this_0 Int))
(=> (= error_0 0) (nondet_interface_1_I_4_0 error_0 this_0))))