diff --git a/Cargo.toml b/Cargo.toml index 77d9a62..de058ac 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,3 +11,5 @@ num-bigint = "^0.4.3" tempfile = "3" clap = "^3.2" num-traits = "^0.2.15" +colored = "^2" +codespan-reporting = "^0.11.1" \ No newline at end of file diff --git a/src/encoder.rs b/src/encoder.rs index 927402f..d5fb388 100644 --- a/src/encoder.rs +++ b/src/encoder.rs @@ -1,4 +1,5 @@ use crate::evm_context; +use crate::execution_position::ExecutionPositionManager; use crate::smt::{self, SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable}; use crate::ssa_tracker::SSATracker; @@ -29,6 +30,7 @@ pub struct Encoder { interpreter: InstructionsType, loop_unroll: u64, path_conditions: Vec, + execution_position: ExecutionPositionManager, } pub fn encode(ast: &Block, loop_unroll: u64) -> String { @@ -51,23 +53,27 @@ pub fn encode_revert_reachable( encoder.encode(ast, loop_unroll); encoder.encode_revert_reachable(); - encode_with_counterexamples(encoder, counterexamples) + encode_with_counterexamples(&mut encoder, counterexamples) } pub fn encode_solc_panic_reachable( ast: &Block, loop_unroll: u64, counterexamples: &[Expression], -) -> (String, Vec) { +) -> (String, Vec, String, ExecutionPositionManager) { let mut encoder = Encoder::::default(); encoder.encode(ast, loop_unroll); encoder.encode_solc_panic_reachable(); + let revert_position = ExecutionPositionManager::smt_variable() + .smt_var(&mut encoder.ssa_tracker) + .as_smt(); - encode_with_counterexamples(encoder, counterexamples) + let (enc, cex) = encode_with_counterexamples(&mut encoder, counterexamples); + (enc, cex, revert_position, encoder.execution_position) } fn encode_with_counterexamples( - mut encoder: Encoder, + encoder: &mut Encoder, counterexamples: &[Expression], ) -> (String, Vec) { let encoded_counterexamples = counterexamples @@ -110,7 +116,8 @@ impl Encoder { } fn encode_context_init(&mut self) { - let output = evm_context::init(&mut self.ssa_tracker); + let mut output = evm_context::init(&mut self.ssa_tracker); + output.push(ExecutionPositionManager::init(&mut self.ssa_tracker)); self.out_vec(output); } @@ -138,6 +145,7 @@ impl Encoder { value: None, location: None, }); + self.encode_block(&function.body); self.ssa_tracker.to_smt_variables(&function.returns) } @@ -312,7 +320,23 @@ impl Encoder { .rev() .collect(); - match call.function.id { + let record_location = match call.function.id { + IdentifierID::Reference(_) => true, + IdentifierID::BuiltinReference => call.function.name == "revert", // TODO more flexibility about which builtins to record. + _ => false, + }; + + if record_location { + self.execution_position.function_called(call); + let record_pos = evm_context::assign_variable_if_executing_regularly( + &mut self.ssa_tracker, + &ExecutionPositionManager::smt_variable(), + self.execution_position.position_id().into(), + ); + self.out(record_pos); + } + + let return_vars = match call.function.id { IdentifierID::BuiltinReference => { let builtin = &InstructionsType::builtin(&call.function.name).unwrap(); let return_vars: Vec = (0..builtin.returns) @@ -337,7 +361,18 @@ impl Encoder { "Unexpected reference in function call: {:?}", call.function.id ), + }; + + if record_location { + self.execution_position.function_returned(); + let record_pos = evm_context::assign_variable_if_executing_regularly( + &mut self.ssa_tracker, + &ExecutionPositionManager::smt_variable(), + self.execution_position.position_id().into(), + ); + self.out(record_pos); } + return_vars } } diff --git a/src/evm_context.rs b/src/evm_context.rs index a966f3b..4144b09 100644 --- a/src/evm_context.rs +++ b/src/evm_context.rs @@ -90,7 +90,7 @@ context_variables! { stop_flag: Type::Default; Some(0.into()), revert_flag: Type::Default; Some(0.into()), revert_sig_4: Type::Constant(smt::bv(32)); None, - revert_data_32: Type::Constant(smt::bv(256)); None + revert_data_32: Type::Default; None } // TODO can we make this a global variable? @@ -422,7 +422,7 @@ pub fn encode_solc_panic_reachable(ssa: &mut SSATracker) -> SMTStatement { /// Assigns to the variable if we neither stopped nor reverted. Otherwise, the variable keeps /// its value. Increases the SSA index in any case. -fn assign_variable_if_executing_regularly( +pub fn assign_variable_if_executing_regularly( ssa: &mut SSATracker, variable: &SystemVariable, new_value: SMTExpr, diff --git a/src/execution_position.rs b/src/execution_position.rs new file mode 100644 index 0000000..62ddffe --- /dev/null +++ b/src/execution_position.rs @@ -0,0 +1,80 @@ +use yultsur::yul::{FunctionCall, Identifier, IdentifierID, SourceLocation}; + +use crate::smt::{self, SMTExpr}; +use crate::ssa_tracker::SSATracker; +use crate::variables::SystemVariable; + +/** + * Stores the current call stack encoded in a single number that can be used + * during the SMT encoding. + * + * Can be extended in the future with other information like loop iterations. + */ +#[derive(Default)] +pub struct ExecutionPositionManager { + positions: Vec, +} + +pub struct PositionID(pub usize); + +impl From for SMTExpr { + fn from(pos: PositionID) -> Self { + (pos.0 as u64).into() + } +} + +struct ExecutionPosition { + call_stack: Vec>, +} + +impl ExecutionPositionManager { + pub fn init(ssa_tracker: &mut SSATracker) -> smt::SMTStatement { + Self::smt_variable().generate_definition(ssa_tracker) + } + + /// @returns the SystemVariable that encodes the position. + pub fn smt_variable() -> SystemVariable { + SystemVariable { + identifier: Identifier { + id: IdentifierID::Reference(8128), + name: "_exe_pos".to_string(), + location: None, + }, + domain: vec![], + codomain: smt::bv(256), + default_value: Some(0.into()), + } + } + + pub fn function_called(&mut self, fun: &FunctionCall) { + self.append_position(ExecutionPosition { + call_stack: [self.current_call_stack(), vec![fun.location.clone()]].concat(), + }); + } + + pub fn function_returned(&mut self) { + let mut call_stack = self.current_call_stack(); + call_stack.pop().unwrap(); + self.append_position(ExecutionPosition { call_stack }) + } + + /// Returns the current position ID that can later + /// be translated into e.g. a call stack. + pub fn position_id(&self) -> PositionID { + PositionID(self.positions.len() - 1) + } + + pub fn call_stack_at_position(&self, pos: PositionID) -> &Vec> { + &self.positions[pos.0].call_stack + } + + fn append_position(&mut self, pos: ExecutionPosition) { + self.positions.push(pos) + } + fn current_call_stack(&self) -> Vec> { + match self.positions.iter().last() { + Some(p) => p.call_stack.clone(), + None => vec![], + } + } +} diff --git a/src/lib.rs b/src/lib.rs index 967daea..ed358d4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2,6 +2,7 @@ pub mod cfg; pub mod encoder; pub mod evm_builtins; pub mod evm_context; +pub mod execution_position; pub mod sexpr; pub mod smt; pub mod solver; diff --git a/src/main.rs b/src/main.rs index e9f1cc0..f8140df 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,10 +1,14 @@ use std::env; use std::path::PathBuf; +use codespan_reporting::term::termcolor::WriteColor; +use colored::Colorize; +use num_traits::ToPrimitive; use yools::evm_builtins::EVMInstructions; -use yools::solver; +use yools::{execution_position, solver}; use yultsur::resolver::resolve; +use yultsur::yul::SourceLocation; use yultsur::yul_parser; use yultsur::{dialect::EVMDialect, resolver::resolve_inside}; @@ -26,7 +30,7 @@ fn cli() -> Result<(), String> { .get_matches(); match matches.subcommand() { - Some(("symbolic", sub_matches)) => symbolic_revert(sub_matches), + Some(("symbolic", sub_matches)) => symbolic_revert_cli(sub_matches), _ => unreachable!(), } } @@ -74,13 +78,10 @@ fn symbolic_subcommand() -> App<'static> { ) } -fn symbolic_revert(sub_matches: &ArgMatches) -> Result<(), String> { +fn symbolic_revert_cli(sub_matches: &ArgMatches) -> Result<(), String> { let yul_file = PathBuf::from(sub_matches.value_of("input").unwrap()); - let content = std::fs::read_to_string(yul_file).unwrap(); - - let mut ast = yul_parser::parse_block(&content)?; - resolve::(&mut ast)?; + let source = std::fs::read_to_string(yul_file).unwrap(); let loop_unroll: u64 = sub_matches .value_of("loop-unroll") @@ -96,6 +97,27 @@ fn symbolic_revert(sub_matches: &ArgMatches) -> Result<(), String> { vec![] }; + use codespan_reporting::term::termcolor; + let mut output = termcolor::StandardStream::stdout(termcolor::ColorChoice::Always); + symbolic_revert( + &source, + loop_unroll, + sub_matches.value_of("solver").unwrap(), + eval_strings, + &mut output, + ) +} + +fn symbolic_revert( + source: &str, + loop_unroll: u64, + solver: &str, + eval_strings: Vec, + output: &mut dyn codespan_reporting::term::termcolor::WriteColor, +) -> Result<(), String> { + let mut ast = yul_parser::parse_block(source)?; + resolve::(&mut ast)?; + let counterexamples = eval_strings .iter() .map(|eval| { @@ -104,31 +126,135 @@ fn symbolic_revert(sub_matches: &ArgMatches) -> Result<(), String> { Ok(expr) }) .collect::, String>>()?; - let (query, counterexamples_encoded) = yools::encoder::encode_solc_panic_reachable::< - EVMInstructions, - >(&ast, loop_unroll, &counterexamples); + let (query, counterexamples_encoded, panic_position, position_manager) = + yools::encoder::encode_solc_panic_reachable::( + &ast, + loop_unroll, + &counterexamples, + ); - let solver = solver::SolverConfig::new(sub_matches.value_of("solver").unwrap()); - let (result, values) = - solver::query_smt_with_solver_and_eval(&query, &counterexamples_encoded, solver); + let cex = [counterexamples_encoded, [panic_position].to_vec()].concat(); + let solver = solver::SolverConfig::new(solver); + let (result, mut values) = solver::query_smt_with_solver_and_eval(&query, &cex, solver); match result { true => { - println!("Revert is reachable."); + let panic_position = values.pop().unwrap(); + if let solver::ModelValue::Number(position) = panic_position { + print_detailed_diagnostics( + source, + position_manager.call_stack_at_position(execution_position::PositionID( + position.to_usize().unwrap(), + )), + output, + ); + } else { + write!(output, "Panic is reachable.").unwrap(); + } if !eval_strings.is_empty() { - println!( - "Evaluated expressions:\n{}", + write!( + output, + "{}\n{}", + "Evaluated expressions:".bright_yellow(), eval_strings .iter() .zip(values.iter()) .map(|(s, v)| { format!("{} = {}", s, v) }) .collect::>() .join("\n") - ); + ) + .unwrap(); } } false => { - println!("All reverts are unreachable."); + write!(output, "All panics are unreachable.").unwrap(); } } Ok(()) } + +fn print_detailed_diagnostics( + source: &str, + call_stack: &[Option], + output: &mut dyn WriteColor, +) { + use codespan_reporting as cs; + use cs::diagnostic::{Diagnostic, Label}; + use cs::files::SimpleFiles; + + let config = codespan_reporting::term::Config::default(); + let mut files = SimpleFiles::new(); + let file_id = files.add("input", source); + if let [stack @ .., Some(pos)] = call_stack { + let diagnostic = Diagnostic::error() + .with_message("Panic is reachable.") + .with_labels(vec![Label::primary(file_id, pos.start..pos.end) + .with_message("This revert causes a panic.")]); + cs::term::emit(output, &config, &files, &diagnostic).unwrap(); + for (depth, pos) in stack.iter().rev().enumerate() { + let mut diagnostic = + Diagnostic::note().with_message(format!("Stack level {}:", depth + 1)); + diagnostic = match pos { + Some(pos) => { + diagnostic.with_labels(vec![Label::primary(file_id, (pos.start)..(pos.end)) + .with_message("Called from here.")]) + } + None => diagnostic, + }; + cs::term::emit(output, &config, &files, &diagnostic).unwrap(); + } + } else { + panic!(); + } +} + +#[cfg(test)] +mod test { + use codespan_reporting::term::termcolor; + use std::io::BufWriter; + + use super::*; + + #[test] + fn stack_trace() { + let source = concat!( + "{\n", + " function f() {\n", + " mstore(0, 35408467139433450592217433187231851964531694900788300625387963629091585785856)\n", + " mstore(4, 0x11)\n", + " revert(0, 0x24)\n", + " }\n", + " function g() {\n", + " f()\n", + " }\n", + " g()\n", + "}\n" + ).to_string(); + let mut output = termcolor::NoColor::new(BufWriter::new(Vec::new())); + symbolic_revert(&source, 1, "z3", vec![], &mut output).unwrap(); + let output_str = std::str::from_utf8(output.get_ref().buffer()).unwrap(); + println!("{}", output_str); + assert_eq!( + output_str, + concat!( + "error: Panic is reachable.\n", + " ┌─ input:5:5\n", + " │\n", + "5 │ revert(0, 0x24)\n", + " │ ^^^^^^^^^^^^^^^ This revert causes a panic.\n", + "\n", + "note: Stack level 1:\n", + " ┌─ input:8:5\n", + " │\n", + "8 │ f()\n", + " │ ^^^ Called from here.\n", + "\n", + "note: Stack level 2:\n", + " ┌─ input:10:3\n", + " │\n", + "10 │ g()\n", + " │ ^^^ Called from here.\n", + "\n" + ) + ); + } +} diff --git a/tests/assert_pass/arith_add_1.yul.smt2 b/tests/assert_pass/arith_add_1.yul.smt2 index a0aaef1..7d02752 100644 --- a/tests/assert_pass/arith_add_1.yul.smt2 +++ b/tests/assert_pass/arith_add_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) _address_2048_0) diff --git a/tests/assert_pass/assignments_1.yul.smt2 b/tests/assert_pass/assignments_1.yul.smt2 index f740a5b..ef1b940 100644 --- a/tests/assert_pass/assignments_1.yul.smt2 +++ b/tests/assert_pass/assignments_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) diff --git a/tests/assert_pass/big_decimals.yul.smt2 b/tests/assert_pass/big_decimals.yul.smt2 index 930836b..4c821d6 100644 --- a/tests/assert_pass/big_decimals.yul.smt2 +++ b/tests/assert_pass/big_decimals.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) diff --git a/tests/assert_pass/branches_1.yul.smt2 b/tests/assert_pass/branches_1.yul.smt2 index 71f992e..81b48fe 100644 --- a/tests/assert_pass/branches_1.yul.smt2 +++ b/tests/assert_pass/branches_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _address_2048_0) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000014) diff --git a/tests/assert_pass/branches_memory.yul.smt2 b/tests/assert_pass/branches_memory.yul.smt2 index 790d19a..35b46d3 100644 --- a/tests/assert_pass/branches_memory.yul.smt2 +++ b/tests/assert_pass/branches_memory.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _address_2048_0) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/branches_new_variables.yul.smt2 b/tests/assert_pass/branches_new_variables.yul.smt2 index 28e5cf2..ae62f0b 100644 --- a/tests/assert_pass/branches_new_variables.yul.smt2 +++ b/tests/assert_pass/branches_new_variables.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/byte.yul.smt2 b/tests/assert_pass/byte.yul.smt2 index c8f52b5..582b4de 100644 --- a/tests/assert_pass/byte.yul.smt2 +++ b/tests/assert_pass/byte.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000001234) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/calldata_immutable.yul.smt2 b/tests/assert_pass/calldata_immutable.yul.smt2 index 57a0eca..8be64a4 100644 --- a/tests/assert_pass/calldata_immutable.yul.smt2 +++ b/tests/assert_pass/calldata_immutable.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/calldata_shifted.yul.smt2 b/tests/assert_pass/calldata_shifted.yul.smt2 index 1bd8e38..b493e99 100644 --- a/tests/assert_pass/calldata_shifted.yul.smt2 +++ b/tests/assert_pass/calldata_shifted.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/calldataload_at_calldatasize.yul.smt2 b/tests/assert_pass/calldataload_at_calldatasize.yul.smt2 index 6eb232d..2405cf1 100644 --- a/tests/assert_pass/calldataload_at_calldatasize.yul.smt2 +++ b/tests/assert_pass/calldataload_at_calldatasize.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _calldatasize_2050_0) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/for_loop_1.yul.smt2 b/tests/assert_pass/for_loop_1.yul.smt2 index a984536..ab81aca 100644 --- a/tests/assert_pass/for_loop_1.yul.smt2 +++ b/tests/assert_pass/for_loop_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000003) diff --git a/tests/assert_pass/for_loop_2.yul.smt2 b/tests/assert_pass/for_loop_2.yul.smt2 index 34d9a51..ba84b23 100644 --- a/tests/assert_pass/for_loop_2.yul.smt2 +++ b/tests/assert_pass/for_loop_2.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000003) diff --git a/tests/assert_pass/for_loop_3.yul.smt2 b/tests/assert_pass/for_loop_3.yul.smt2 index 5c8c0b4..c7df5ac 100644 --- a/tests/assert_pass/for_loop_3.yul.smt2 +++ b/tests/assert_pass/for_loop_3.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000003) diff --git a/tests/assert_pass/for_loop_nested_1.yul.smt2 b/tests/assert_pass/for_loop_nested_1.yul.smt2 index 02e38ba..a1c3afe 100644 --- a/tests/assert_pass/for_loop_nested_1.yul.smt2 +++ b/tests/assert_pass/for_loop_nested_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/for_loop_nested_2.yul.smt2 b/tests/assert_pass/for_loop_nested_2.yul.smt2 index 674f6e0..6958cbb 100644 --- a/tests/assert_pass/for_loop_nested_2.yul.smt2 +++ b/tests/assert_pass/for_loop_nested_2.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/for_loop_nested_3.yul.smt2 b/tests/assert_pass/for_loop_nested_3.yul.smt2 index a882c1c..e88404d 100644 --- a/tests/assert_pass/for_loop_nested_3.yul.smt2 +++ b/tests/assert_pass/for_loop_nested_3.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/for_loop_over.yul.smt2 b/tests/assert_pass/for_loop_over.yul.smt2 index 8090cd4..0b3d5c8 100644 --- a/tests/assert_pass/for_loop_over.yul.smt2 +++ b/tests/assert_pass/for_loop_over.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const max_2_1 (_ BitVec 256) _2) @@ -32,12 +33,15 @@ (define-const _4 (_ BitVec 256) (ite (bvugt max_2_1 _3) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (define-const _5 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _6 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const _revert_sig_4_2071_1 (_ BitVec 32) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (bvuge _6 #x0000000000000000000000000000000000000000000000000000000000000004) (concat (select _memory_2063_0 (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000003))) #x00000000) _revert_sig_4_2071_0)) (define-const _revert_data_32_2072_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (= _6 #x0000000000000000000000000000000000000000000000000000000000000024) (concat (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000003)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000004)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000005)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000006)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000007)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000008)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000009)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000a)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000b)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000c)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000d)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000e)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000f)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000010)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000011)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000012)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000013)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000014)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000015)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000016)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000017)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000018)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000019)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001a)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001b)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001c)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001d)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001e)) (select _memory_2063_0 (bvadd (bvadd _5 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001f))) #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_0)) (define-const _revert_flag_2070_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _revert_flag_2070_0)) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_1 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) (define-const _revert_flag_2070_2 (_ BitVec 256) (ite (= _4 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_flag_2070_0 _revert_flag_2070_1)) (define-const _revert_sig_4_2071_2 (_ BitVec 32) (ite (= _4 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_sig_4_2071_0 _revert_sig_4_2071_1)) (define-const _revert_data_32_2072_2 (_ BitVec 256) (ite (= _4 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_0 _revert_data_32_2072_1)) +(define-const _exe_pos_8128_3 (_ BitVec 256) (ite (= _4 #x0000000000000000000000000000000000000000000000000000000000000000) _exe_pos_8128_0 _exe_pos_8128_2)) (define-const _7 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_3_1 (_ BitVec 256) _7) (define-const _8 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/for_loop_under.yul.smt2 b/tests/assert_pass/for_loop_under.yul.smt2 index 809e743..aaaf4c5 100644 --- a/tests/assert_pass/for_loop_under.yul.smt2 +++ b/tests/assert_pass/for_loop_under.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const max_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/function_call_1.yul.smt2 b/tests/assert_pass/function_call_1.yul.smt2 index ef899c1..77b1ff8 100644 --- a/tests/assert_pass/function_call_1.yul.smt2 +++ b/tests/assert_pass/function_call_1.yul.smt2 @@ -25,12 +25,15 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _address_2048_0) (define-const x_5_1 (_ BitVec 256) _1) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const a_3_0 (_ BitVec 256) x_5_1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const b_4_1 (_ BitVec 256) _2) (define-const b_4_2 (_ BitVec 256) a_3_0) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) (define-const _3 (_ BitVec 256) (ite (= x_5_1 b_4_2) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (assert (and (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) true (= _3 #x0000000000000000000000000000000000000000000000000000000000000000))) (assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000))) \ No newline at end of file diff --git a/tests/assert_pass/function_call_add_1.yul.smt2 b/tests/assert_pass/function_call_add_1.yul.smt2 index ff34c37..3043f44 100644 --- a/tests/assert_pass/function_call_add_1.yul.smt2 +++ b/tests/assert_pass/function_call_add_1.yul.smt2 @@ -25,10 +25,12 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _address_2048_0) (define-const x_6_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) _address_2048_0) (define-const y_7_1 (_ BitVec 256) _2) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const a_3_0 (_ BitVec 256) x_6_1) (define-const b_4_0 (_ BitVec 256) y_7_1) (define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) @@ -37,24 +39,31 @@ (define-const _5 (_ BitVec 256) (ite (bvugt a_3_0 _4) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (define-const _6 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _7 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) (define-const _revert_sig_4_2071_1 (_ BitVec 32) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (bvuge _7 #x0000000000000000000000000000000000000000000000000000000000000004) (concat (select _memory_2063_0 (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000003))) #x00000000) _revert_sig_4_2071_0)) (define-const _revert_data_32_2072_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (= _7 #x0000000000000000000000000000000000000000000000000000000000000024) (concat (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000003)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000004)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000005)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000006)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000007)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000008)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000009)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000a)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000b)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000c)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000d)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000e)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000f)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000010)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000011)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000012)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000013)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000014)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000015)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000016)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000017)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000018)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000019)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001a)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001b)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001c)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001d)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001e)) (select _memory_2063_0 (bvadd (bvadd _6 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001f))) #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_0)) (define-const _revert_flag_2070_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _revert_flag_2070_0)) +(define-const _exe_pos_8128_3 (_ BitVec 256) (ite (and (= _revert_flag_2070_1 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000002 _exe_pos_8128_2)) (define-const _revert_flag_2070_2 (_ BitVec 256) (ite (= _5 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_flag_2070_0 _revert_flag_2070_1)) (define-const _revert_sig_4_2071_2 (_ BitVec 32) (ite (= _5 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_sig_4_2071_0 _revert_sig_4_2071_1)) (define-const _revert_data_32_2072_2 (_ BitVec 256) (ite (= _5 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_0 _revert_data_32_2072_1)) +(define-const _exe_pos_8128_4 (_ BitVec 256) (ite (= _5 #x0000000000000000000000000000000000000000000000000000000000000000) _exe_pos_8128_1 _exe_pos_8128_3)) (define-const _8 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000064) (define-const _9 (_ BitVec 256) (ite (bvugt b_4_0 _8) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (define-const _10 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _11 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) +(define-const _exe_pos_8128_5 (_ BitVec 256) (ite (and (= _revert_flag_2070_2 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000003 _exe_pos_8128_4)) (define-const _revert_sig_4_2071_3 (_ BitVec 32) (ite (and (= _revert_flag_2070_2 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (bvuge _11 #x0000000000000000000000000000000000000000000000000000000000000004) (concat (select _memory_2063_0 (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000003))) #x00000000) _revert_sig_4_2071_2)) (define-const _revert_data_32_2072_3 (_ BitVec 256) (ite (and (= _revert_flag_2070_2 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (= _11 #x0000000000000000000000000000000000000000000000000000000000000024) (concat (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000003)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000004)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000005)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000006)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000007)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000008)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000009)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000a)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000b)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000c)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000d)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000e)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000f)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000010)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000011)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000012)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000013)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000014)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000015)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000016)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000017)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000018)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000019)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001a)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001b)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001c)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001d)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001e)) (select _memory_2063_0 (bvadd (bvadd _10 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001f))) #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_2)) (define-const _revert_flag_2070_3 (_ BitVec 256) (ite (and (= _revert_flag_2070_2 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _revert_flag_2070_2)) +(define-const _exe_pos_8128_6 (_ BitVec 256) (ite (and (= _revert_flag_2070_3 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000004 _exe_pos_8128_5)) (define-const _revert_flag_2070_4 (_ BitVec 256) (ite (= _9 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_flag_2070_2 _revert_flag_2070_3)) (define-const _revert_sig_4_2071_4 (_ BitVec 32) (ite (= _9 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_sig_4_2071_2 _revert_sig_4_2071_3)) (define-const _revert_data_32_2072_4 (_ BitVec 256) (ite (= _9 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_2 _revert_data_32_2072_3)) +(define-const _exe_pos_8128_7 (_ BitVec 256) (ite (= _9 #x0000000000000000000000000000000000000000000000000000000000000000) _exe_pos_8128_4 _exe_pos_8128_6)) (define-const _12 (_ BitVec 256) (bvadd a_3_0 b_4_0)) (define-const c_5_2 (_ BitVec 256) _12) +(define-const _exe_pos_8128_8 (_ BitVec 256) (ite (and (= _revert_flag_2070_4 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000005 _exe_pos_8128_7)) (define-const _13 (_ BitVec 256) (ite (bvugt x_6_1 c_5_2) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (define-const _14 (_ BitVec 256) (ite (= _13 #x0000000000000000000000000000000000000000000000000000000000000000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (assert (and (and (= _revert_flag_2070_4 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) true (= _14 #x0000000000000000000000000000000000000000000000000000000000000000))) diff --git a/tests/assert_pass/inside_for_1.yul.smt2 b/tests/assert_pass/inside_for_1.yul.smt2 index d8eeb56..dc309d1 100644 --- a/tests/assert_pass/inside_for_1.yul.smt2 +++ b/tests/assert_pass/inside_for_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/inside_if_1.yul.smt2 b/tests/assert_pass/inside_if_1.yul.smt2 index 9164402..6f61760 100644 --- a/tests/assert_pass/inside_if_1.yul.smt2 +++ b/tests/assert_pass/inside_if_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/inside_if_nested_1.yul.smt2 b/tests/assert_pass/inside_if_nested_1.yul.smt2 index 0a7988a..4009c05 100644 --- a/tests/assert_pass/inside_if_nested_1.yul.smt2 +++ b/tests/assert_pass/inside_if_nested_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/inside_switch_1.yul.smt2 b/tests/assert_pass/inside_switch_1.yul.smt2 index 908a485..37935b2 100644 --- a/tests/assert_pass/inside_switch_1.yul.smt2 +++ b/tests/assert_pass/inside_switch_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/inside_switch_2.yul.smt2 b/tests/assert_pass/inside_switch_2.yul.smt2 index 21a7752..e1b678b 100644 --- a/tests/assert_pass/inside_switch_2.yul.smt2 +++ b/tests/assert_pass/inside_switch_2.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/inside_switch_3.yul.smt2 b/tests/assert_pass/inside_switch_3.yul.smt2 index ce2592d..83c2da2 100644 --- a/tests/assert_pass/inside_switch_3.yul.smt2 +++ b/tests/assert_pass/inside_switch_3.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/large_hex_constants_wrapping_1.yul.smt2 b/tests/assert_pass/large_hex_constants_wrapping_1.yul.smt2 index 52a47e2..5dd7578 100644 --- a/tests/assert_pass/large_hex_constants_wrapping_1.yul.smt2 +++ b/tests/assert_pass/large_hex_constants_wrapping_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) diff --git a/tests/assert_pass/memory_not_cleared_for_zero_length_call.yul.smt2 b/tests/assert_pass/memory_not_cleared_for_zero_length_call.yul.smt2 index c5b35c5..27a2f6c 100644 --- a/tests/assert_pass/memory_not_cleared_for_zero_length_call.yul.smt2 +++ b/tests/assert_pass/memory_not_cleared_for_zero_length_call.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000009) (define-const _memory_2063_1 (Array (_ BitVec 256) (_ BitVec 8)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store _memory_2063_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) ((_ extract 255 248) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) ((_ extract 247 240) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) ((_ extract 239 232) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) ((_ extract 231 224) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) ((_ extract 223 216) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) ((_ extract 215 208) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) ((_ extract 207 200) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) ((_ extract 199 192) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) ((_ extract 191 184) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) ((_ extract 183 176) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) ((_ extract 175 168) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) ((_ extract 167 160) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) ((_ extract 159 152) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) ((_ extract 151 144) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) ((_ extract 143 136) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) ((_ extract 135 128) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) ((_ extract 127 120) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) ((_ extract 119 112) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) ((_ extract 111 104) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) ((_ extract 103 96) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) ((_ extract 95 88) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) ((_ extract 87 80) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) ((_ extract 79 72) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) ((_ extract 71 64) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) ((_ extract 63 56) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) ((_ extract 55 48) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) ((_ extract 47 40) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) ((_ extract 39 32) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) ((_ extract 31 24) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) ((_ extract 23 16) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) ((_ extract 15 8) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) ((_ extract 7 0) _2))) diff --git a/tests/assert_pass/mstore8.yul.smt2 b/tests/assert_pass/mstore8.yul.smt2 index 285444d..7940433 100644 --- a/tests/assert_pass/mstore8.yul.smt2 +++ b/tests/assert_pass/mstore8.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) (define-const i_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000001234) diff --git a/tests/assert_pass/mstore_mload.yul.smt2 b/tests/assert_pass/mstore_mload.yul.smt2 index 25f0c7b..9af6221 100644 --- a/tests/assert_pass/mstore_mload.yul.smt2 +++ b/tests/assert_pass/mstore_mload.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000008) (define-const _memory_2063_1 (Array (_ BitVec 256) (_ BitVec 8)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store _memory_2063_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) ((_ extract 255 248) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) ((_ extract 247 240) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) ((_ extract 239 232) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) ((_ extract 231 224) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) ((_ extract 223 216) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) ((_ extract 215 208) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) ((_ extract 207 200) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) ((_ extract 199 192) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) ((_ extract 191 184) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) ((_ extract 183 176) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) ((_ extract 175 168) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) ((_ extract 167 160) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) ((_ extract 159 152) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) ((_ extract 151 144) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) ((_ extract 143 136) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) ((_ extract 135 128) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) ((_ extract 127 120) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) ((_ extract 119 112) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) ((_ extract 111 104) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) ((_ extract 103 96) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) ((_ extract 95 88) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) ((_ extract 87 80) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) ((_ extract 79 72) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) ((_ extract 71 64) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) ((_ extract 63 56) _2)) (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) ((_ extract 55 48) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) ((_ extract 47 40) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) ((_ extract 39 32) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) ((_ extract 31 24) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) ((_ extract 23 16) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) ((_ extract 15 8) _2)) (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) ((_ extract 7 0) _2))) diff --git a/tests/assert_pass/selfbalance_unchanged_after_failed_call.yul.smt2 b/tests/assert_pass/selfbalance_unchanged_after_failed_call.yul.smt2 index dc9d8f2..606b6d9 100644 --- a/tests/assert_pass/selfbalance_unchanged_after_failed_call.yul.smt2 +++ b/tests/assert_pass/selfbalance_unchanged_after_failed_call.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _selfbalance_2062_0) (define-const b_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000002710) diff --git a/tests/assert_pass/small_eq.yul.smt2 b/tests/assert_pass/small_eq.yul.smt2 index 1067450..3d348c2 100644 --- a/tests/assert_pass/small_eq.yul.smt2 +++ b/tests/assert_pass/small_eq.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/small_eq_unreach.yul.smt2 b/tests/assert_pass/small_eq_unreach.yul.smt2 index b5e83d7..3073489 100644 --- a/tests/assert_pass/small_eq_unreach.yul.smt2 +++ b/tests/assert_pass/small_eq_unreach.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _stop_flag_2069_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _stop_flag_2069_0)) diff --git a/tests/assert_pass/small_eq_unreach_revert.yul.smt2 b/tests/assert_pass/small_eq_unreach_revert.yul.smt2 index bb15136..14806b2 100644 --- a/tests/assert_pass/small_eq_unreach_revert.yul.smt2 +++ b/tests/assert_pass/small_eq_unreach_revert.yul.smt2 @@ -25,13 +25,16 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const _revert_sig_4_2071_1 (_ BitVec 32) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (bvuge _3 #x0000000000000000000000000000000000000000000000000000000000000004) (concat (select _memory_2063_0 (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000003))) #x00000000) _revert_sig_4_2071_0)) (define-const _revert_data_32_2072_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) (ite (= _3 #x0000000000000000000000000000000000000000000000000000000000000024) (concat (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000000)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000001)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000002)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000003)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000004)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000005)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000006)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000007)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000008)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000009)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000a)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000b)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000c)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000d)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000e)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000000f)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000010)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000011)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000012)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000013)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000014)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000015)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000016)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000017)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000018)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x0000000000000000000000000000000000000000000000000000000000000019)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001a)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001b)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001c)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001d)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001e)) (select _memory_2063_0 (bvadd (bvadd _2 #x0000000000000000000000000000000000000000000000000000000000000004) #x000000000000000000000000000000000000000000000000000000000000001f))) #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_0)) (define-const _revert_flag_2070_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _revert_flag_2070_0)) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_1 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) (define-const _4 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) (define-const _5 (_ BitVec 256) (ite (= x_2_1 _4) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000)) (assert (and (and (= _revert_flag_2070_1 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) true (= _5 #x0000000000000000000000000000000000000000000000000000000000000000))) diff --git a/tests/assert_pass/storage.yul.smt2 b/tests/assert_pass/storage.yul.smt2 index 48401f0..df017da 100644 --- a/tests/assert_pass/storage.yul.smt2 +++ b/tests/assert_pass/storage.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) (define-const _storage_2064_1 (Array (_ BitVec 256) (_ BitVec 256)) (store _storage_2064_0 _1 _2)) diff --git a/tests/assert_pass/storage_not_cleared_after_failed_call.yul.smt2 b/tests/assert_pass/storage_not_cleared_after_failed_call.yul.smt2 index a5420da..78b95de 100644 --- a/tests/assert_pass/storage_not_cleared_after_failed_call.yul.smt2 +++ b/tests/assert_pass/storage_not_cleared_after_failed_call.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000007) (define-const _storage_2064_1 (Array (_ BitVec 256) (_ BitVec 256)) (store _storage_2064_0 _1 _2)) diff --git a/tests/assert_pass/switch.yul.smt2 b/tests/assert_pass/switch.yul.smt2 index f5391df..f5100ef 100644 --- a/tests/assert_pass/switch.yul.smt2 +++ b/tests/assert_pass/switch.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/assert_pass/switch_1.yul.smt2 b/tests/assert_pass/switch_1.yul.smt2 index 05b9750..56fe046 100644 --- a/tests/assert_pass/switch_1.yul.smt2 +++ b/tests/assert_pass/switch_1.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) diff --git a/tests/assert_pass/switch_2.yul.smt2 b/tests/assert_pass/switch_2.yul.smt2 index 340177c..736afc0 100644 --- a/tests/assert_pass/switch_2.yul.smt2 +++ b/tests/assert_pass/switch_2.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) diff --git a/tests/assert_pass/switch_3.yul.smt2 b/tests/assert_pass/switch_3.yul.smt2 index c0b3a00..d474cdd 100644 --- a/tests/assert_pass/switch_3.yul.smt2 +++ b/tests/assert_pass/switch_3.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) (define-const x_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) diff --git a/tests/assert_pass/zero_init.yul.smt2 b/tests/assert_pass/zero_init.yul.smt2 index 78a3b6d..e90798e 100644 --- a/tests/assert_pass/zero_init.yul.smt2 +++ b/tests/assert_pass/zero_init.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const a_2_1 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) diff --git a/tests/assert_pass/zero_init_multi.yul.smt2 b/tests/assert_pass/zero_init_multi.yul.smt2 index 560bc85..471b3e2 100644 --- a/tests/assert_pass/zero_init_multi.yul.smt2 +++ b/tests/assert_pass/zero_init_multi.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const a_2_1 (_ BitVec 256) _1) (define-const b_3_1 (_ BitVec 256) _1) diff --git a/tests/integration.rs b/tests/integration.rs index e804f32..07123ec 100644 --- a/tests/integration.rs +++ b/tests/integration.rs @@ -152,7 +152,7 @@ mod panic_unreachable { // build.rs creates one test per .yul file in the panic_unreachable directory. fn test_panic_unreachable(content: &str, file: &str) { let ast = parse_and_resolve::(content, file); - let (query, _) = encoder::encode_solc_panic_reachable::( + let (query, ..) = encoder::encode_solc_panic_reachable::( &ast, loop_unroll_default(&content), &[], @@ -170,7 +170,7 @@ mod some_panic_reachable { // build.rs creates one test per .yul file in the some_panic_reachable directory. fn test_some_panic_reachable(content: &str, file: &str) { let ast = parse_and_resolve::(content, file); - let (query, _) = encoder::encode_solc_panic_reachable::( + let (query, ..) = encoder::encode_solc_panic_reachable::( &ast, loop_unroll_default(&content), &[], diff --git a/tests/syntax/calldataload.yul.smt2 b/tests/syntax/calldataload.yul.smt2 index a6b9c9b..ab61a40 100644 --- a/tests/syntax/calldataload.yul.smt2 +++ b/tests/syntax/calldataload.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000007) (define-const _2 (_ BitVec 256) (concat (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000000)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000001)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000002)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000003)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000004)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000005)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000006)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000007)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000008)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000009)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000000f)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000010)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000011)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000012)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000013)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000014)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000015)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000016)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000017)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000018)) #x00) (ite (bvult (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x0000000000000000000000000000000000000000000000000000000000000019)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001a)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001b)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001c)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001d)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001e)) #x00) (ite (bvult (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f) _calldatasize_2050_0) (_calldata_2065_0 (bvadd _1 #x000000000000000000000000000000000000000000000000000000000000001f)) #x00))) (define-const x_2_1 (_ BitVec 256) _2) diff --git a/tests/syntax/function_call_1.yul.smt2 b/tests/syntax/function_call_1.yul.smt2 index d88121c..4eb6386 100644 --- a/tests/syntax/function_call_1.yul.smt2 +++ b/tests/syntax/function_call_1.yul.smt2 @@ -25,14 +25,19 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const a_3_0 (_ BitVec 256) _1) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const b_4_1 (_ BitVec 256) _2) (define-const b_4_2 (_ BitVec 256) a_3_0) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) +(define-const _exe_pos_8128_3 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000002 _exe_pos_8128_2)) (define-const a_3_1 (_ BitVec 256) b_4_2) (define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const b_4_4 (_ BitVec 256) _3) (define-const b_4_5 (_ BitVec 256) a_3_1) +(define-const _exe_pos_8128_4 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000003 _exe_pos_8128_3)) (define-const x_5_1 (_ BitVec 256) b_4_5) (assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000))) \ No newline at end of file diff --git a/tests/syntax/function_call_2.yul.smt2 b/tests/syntax/function_call_2.yul.smt2 index a49f191..2edef28 100644 --- a/tests/syntax/function_call_2.yul.smt2 +++ b/tests/syntax/function_call_2.yul.smt2 @@ -25,8 +25,10 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001) (define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002) +(define-const _exe_pos_8128_1 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000000 _exe_pos_8128_0)) (define-const a_3_0 (_ BitVec 256) _1) (define-const b_4_0 (_ BitVec 256) _2) (define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) @@ -34,8 +36,10 @@ (define-const d_6_1 (_ BitVec 256) _3) (define-const c_5_2 (_ BitVec 256) a_3_0) (define-const d_6_2 (_ BitVec 256) b_4_0) +(define-const _exe_pos_8128_2 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000001 _exe_pos_8128_1)) (define-const x_7_1 (_ BitVec 256) c_5_2) (define-const y_8_1 (_ BitVec 256) d_6_2) +(define-const _exe_pos_8128_3 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000002 _exe_pos_8128_2)) (define-const a_3_1 (_ BitVec 256) x_7_1) (define-const b_4_1 (_ BitVec 256) y_8_1) (define-const _4 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) @@ -43,6 +47,7 @@ (define-const d_6_4 (_ BitVec 256) _4) (define-const c_5_5 (_ BitVec 256) a_3_1) (define-const d_6_5 (_ BitVec 256) b_4_1) +(define-const _exe_pos_8128_4 (_ BitVec 256) (ite (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) #x0000000000000000000000000000000000000000000000000000000000000003 _exe_pos_8128_3)) (define-const t_9_1 (_ BitVec 256) c_5_5) (define-const s_10_1 (_ BitVec 256) d_6_5) (assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000))) \ No newline at end of file diff --git a/tests/syntax/keccak.yul.smt2 b/tests/syntax/keccak.yul.smt2 index 3e2770a..8486afe 100644 --- a/tests/syntax/keccak.yul.smt2 +++ b/tests/syntax/keccak.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) _address_2048_0) (define-const _2 (_ BitVec 256) _number_2059_0) (define-const _3 (_ BitVec 256) _difficulty_2056_0) diff --git a/tests/syntax/var_decl.yul.smt2 b/tests/syntax/var_decl.yul.smt2 index 3976469..24e5777 100644 --- a/tests/syntax/var_decl.yul.smt2 +++ b/tests/syntax/var_decl.yul.smt2 @@ -25,6 +25,7 @@ (declare-fun _revert_data_32_2072_0 () (_ BitVec 256)) (assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000)) (assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff)) +(define-fun _exe_pos_8128_0 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000) (define-const a_2_1 (_ BitVec 256) _1) (assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000))) \ No newline at end of file