Sym exec seems not to run in called functions

[ggballas]

This function:

// Function 50
func contracts.account.library.ArgentModel.change_signer{syscall_ptr : felt*, pedersen_ptr : starkware.cairo.common.cairo_builtins.HashBuiltin*, range_check_ptr : felt}(new_signer : felt){
    v591_new_signer = v585_ptr
    assert_only_self()
    v592_callers_function_frame = v588_syscall_ptr
    assert_not_zero(v592_callers_function_frame)
    v593_return_instruction = v589_pedersen_ptr
    v594 = v586_retdata_size
    v595 = v587_retdata
    v596 = v588_syscall_ptr
    write(v596)
    v597 = v594
    v598 = v596
    v599 = v588_syscall_ptr
    emit(v599)
    v600 = v598
    v601 = v573_retdata
    v602 = v599
    ret
}

calls this function:

// Function 2
func starkware.cairo.common.math.assert_not_zero{}(value : felt){
    %{ 
        from starkware.cairo.common.math_utils import assert_integer
        assert_integer(ids.value)
        assert ids.value % PRIME != 0, f'assert_not_zero failed: {ids.value} = 0.'
    %} 
    if (v12 == 0) {
        v12 = 1    // 0x1
    }
    ret
}

When asking thoth to give a possible solution for the function assert_not_zero() for v12, it spits out 1 (which makes sense, because v12 can't be zero):

thoth local ./artifacts/ArgentAccount.json --symbolic -function starkware.cairo.common.math.assert_not_zero -solve v12 -assertions
v12: 1

but when attempting to achieve the same result by calling it on the function change_signer() for v592_callers_function_frame, it gives 0 as a possible solution:

thoth local ./artifacts/ArgentAccount.json --symbolic -function contracts.account.library.ArgentModel.change_signer -solve v592 -assertions
v592: 0

(the variable appears as v592 in the assignations output and not as v592_callers_function_frame, which is why it was called that in the command).

This leads me to conclude that the sym exec doesn't run inside function calls. Is this on purpose? Or is this a bug?

[pventuzelo]

Yes exactly, we are not doing sym exec on function calls otherwise It will explode the complexity. I will also not give proper results since those function calls may be dependent on user inputs. The solution is actually to "simulate" the result of the function call by using the constraint.

we will make a detailed tutorial soon ;)