[BUG] TG-Nonlin: generates tests with incorrect constructor ABIs

[BritikovKI]

Bug report

Bug description

TGNonlin seems to sometimes do not catch the correct interfaces. Specifically, there is a case when it cannot find and assign a correct variable to the constructor, but still somehow produces the model for the tests.

To reproduce

For following files:

• Solidity
• CHC

TGNonlin follows this behavior:

1. Receives a call to run the testgen for contract B:

   ./build/tgnonlin --keys contract_B3_94:state,msg.value,msg.sender,b^f3__75:state,msg.value,msg.sender^g3__93:state,msg.value,msg.sender /Users/konstantin.britikov/Documents/SMT/solidity_testgen/sandbox/constructor_3_updated.smt2

2. Finds a satisfying model, tries to assign at least some values.
3. At lines 659-661 of NonlinCHCsolver.cpp it can't find variable b. Based on the printed tree_map, variable b is not encountered at all.

Expected behaviour

Based on the CHC analysis it should be able to find the value for variable b, because it is a required variable to call a constructor of the B contract.

Files or input data

The running comand:

./build/tgnonlin --keys contract_B3_94:state,msg.value,msg.sender,b^f3__75:state,msg.value,msg.sender^g3__93:state,msg.value,msg.sender /Users/konstantin.britikov/Documents/SMT/solidity_testgen/sandbox/constructor_3_updated.smt2

Additional context

Reason behind this behaviour might be the fact that there are two contracts in the file being tested, and tgnonlin is being confused by the fact, which one to use (partially because one is inherited by another one). This can be because of the encoding... Constructor is found in the tree map and it has a vars instead of bs, B constructor calls on constructor of A, but still, it receives int b as an input, it might be some simplification on the encoding site, but I doubt it tbh

Screenshots

[BritikovKI]

Jic, working on this issue rn

[BritikovKI]

Fixed