Investigate SMT timeout in test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k

[palinatolmach]

As identified in #2260, the kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k fails in the booster CI job consistently with the smt solver error, which the backend team recommended to interpret as an SMT timeout. It, indeed, stops failing if the SMT timeout (--smt-timeout) is increased to 1.6s. The solver transcripts are attached:
timeout-smtlib.kore.txt
timeout-smtlib.txt
timeout-term.txt

The query causing the timeout looks like this (by @PetarMax, from a Slack discussion):

B : supposed to represent 
    ( 115792089237316195423570985008687907853269984665640564039457584007913129639935 /Word ( ( a *Int b ) /Int 1000000000000000000 ) ) <Int 1000000000000000000
    but not encoded as such

Constraints:

(= false (and (not (= a 0 ) ) (< (div 115792089237316195423570985008687907853269984665640564039457584007913129639935 a ) b ) ) ) 
B
(= true (< 0 a ) ) 
(= true (< 0 b ) )
(= true (< CALLER_ID 1461501637330902918203684832716283019655932542976 ) )
(= true (< ORIGIN_ID 1461501637330902918203684832716283019655932542976 ) )
(= true (< a 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) ) 
(= true (< b 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) ) 
(= true (<= 0 CALLER_ID ) )
(= true (<= 0 NUMBER_CELL ) ) 
(= true (<= 0 ORIGIN_ID ) ) 
(= true (<= 0 a ) ) 
(= true (<= 0 b ) ) 
(= true (<= NUMBER_CELL 57896044618658097711785492504343953926634992332820282019728792003956564819967 ) ) 
(= true (<= b (div 115792089237316195423570985008687907853269984665640564039457584007913129639935 a ) ) ) 
(not (= 0 (div (* a b ) 1000000000000000000 ) ) ) 
(not (= a 0 ) ) ) ) ) ) ) ) ) ) )