Sym exec returns solutions when tx should revert

[ggballas]

I ran this command:

thoth local ./artifacts/ArgentAccount.json --symbolic -function contracts.account.library.ArgentModel.initialize -constraint v551_res==1 -solve v556

on this piece of compiled code (full file available as attachment):

// Function 48
func contracts.account.library.ArgentModel.initialize{syscall_ptr : felt*, pedersen_ptr : starkware.cairo.common.cairo_builtins.HashBuiltin*, range_check_ptr : felt}(signer : felt, guardian : felt){
    v548 = v541_syscall_ptr
    v549 = v542_pedersen_ptr
    v550 = v543_range_check_ptr
    let (v551_res) = read()
    assert v551_res = 0    // 0x0
    v552 = v544_signer
    assert_not_zero(v552)
    v553 = v546_callers_function_frame
    v554 = v547_return_instruction
    v555 = v548
    v556 = v544_signer
    write(v556)
    v557 = v545_guardian
    write(v557)
    ret
}

and received a solution (v556: 0). however, the tx would've reverted since v551_res is asserted to be 0 (whereas it was constrained to be 1). to the best of my knowledge Thoth should return No solution.

ArgentAccount.json.zip

[ggballas]

hey fellas, please let me know if a fix for this is planned for anytime soon?

[pventuzelo]

@ggballas It's fixed with version 0.7.0 ;)