Spacer goes into an infinite loop

commit: cf8c198
options: fp.spacer.global=true fp.spacer.gg.conjecture=true fp.spacer.gg.concretize=true fp.spacer.gg.subsume=true fp.xform.slice=true fp.xform.inline_linear=true fp.xform.inline_eager=true fp.xform.tail_simplifier_pve=true fp.engine=spacer fp.print_statistics=false fp.spacer.elim_aux=true fp.spacer.reach_dnf=true fp.spacer.iuc=1 fp.spacer.iuc.arith=1 fp.validate=true fp.spacer.ground_pobs=true fp.spacer.mbqi=false fp.spacer.iuc.print_farkas_stats=false fp.spacer.iuc.old_hyp_reducer=false fp.spacer.ctp=true fp.spacer.native_mbp=true fp.spacer.weak_abs=true fp.spacer.q3=true fp.spacer.q3.use_qgen=true -v:1
benchmarks: https://github.com/leonardoalt/chc_benchmarks_solidity/blob/main/unit_tests/blockchain_state/balance_receive_ext_calls_2.sol_0.smt2
https://github.com/leonardoalt/chc_benchmarks_solidity/blob/main/unit_tests/blockchain_state/balance_receive_ext_calls_2.sol_1.smt2

This is the infinite loop:

For a rule of the form A && B && Tr ==> C. A pob p_C of C is reachable from must summaries of B and may summaries of A. That is, F_A && R_B && Tr && p_C is SAT. But R_A && R_B && Tr && p_C is not SAT.
The predecessor pob p_A = mbp(Tr && p_C, ...) is reachable from INIT.

Provide feedback