[Question] function overloading vs CHCs

[izlatkin]

How it is possible to distinct CHCs from functions with the same name (fun. overloading)?

for example there are summary_3_function_f__30_59_0 and summary_5_function_f__58_59_0

Below is an example of the source file

contract C {

    uint a;

	function f(uint x) public {
		if (x == 0){
			a = a + 1;
		}else{
			a = x;
		}
		assert(a >= 0);
	}

	function f(uint x, uint y) public {
		if (x > y){
			a = x;
		}else{
			a = y;
		}
		assert(a >= 0);
	}
}

encoding:
without adts
overloading_wo_adt.smt2.txt

original
overloading.smt2.txt

[leonardoalt]

In the example above, 30 and 58 are the AST ids of the function definitions, so that can be used to separate the two in the encoding. 59 is the AST id of the contract definition. And 0 is the SSA index of each predicate application

[izlatkin]

@leonardoalt Does it mean that function that is first in the source file has a smaller id? Does json have the same order?

[izlatkin]

If add id of ast node the tgnonlin crashed

/Users/ilyazlatkin/CLionProjects/aeval/cmake-build-debug/tools/nonlin/tgnonlin --keys contract_C:a,b^f_55:_x^f_88:_x,_y constructor_2_fun_overloading.smt2
Assertion failed: (0 && "Unsupported sort"), function unmarshal, file ZExprConverter.hpp, line 571.
Abort trap: 6

[izlatkin]

/Users/ilyazlatkin/CLionProjects/aeval/cmake-build-debug/tools/nonlin/tgnonlin --keys contract_C:a,b^f__55:_x^f__88:_x,_y constructor_2_fun_overloading.smt2
Assertion failed: (0 && "Unsupported sort"), function unmarshal, file ZExprConverter.hpp, line 571.
Abort trap: 6

constructor_2_fun_overloading.smt2.txt

[izlatkin]

also, it crashed with contract_C:a,b^f:_x^f:_x,_y and crashed during parsing