Very slow simple division formula

[Edward Schwartz]

Hi,

I am attaching another stp formula that stp does not solve in a
reasonable amount of time. I've let it run for five minutes, and stp
could not solve it. It seems like it should be solvable in under a
second; other SMTs can do so, so I suspect this is a bug.

Thanks,

Edward

[Trevor Hansen]

> I am attaching another stp formula that stp does not solve in a
> reasonable amount of time.

Hi Edward,

Thanks for the test case, I'm always interested in obvious instances that run slowly. Most of the time, as in this case, it's because there is a simplification rule that STP doesn't implement. I've added the necessary rule into STP.

Thanks for letting us know,

Trev.

% free variables:
R_EAX_5 : BITVECTOR(32);
R_EBX_6 : BITVECTOR(32);
% end free variables.

ASSERT(
0bin1 =
(LET initial_EBX_82_0 = R_EBX_6 IN
(LET initial_EAX_83_1 = R_EAX_5 IN
(LET temp_96_2 = (​0bin00000000000000000000000000​000000 @ R_EAX_5) IN
(LET temp_98_3 = (​0bin00000000000000000000000000​000000 @ R_EBX_6) IN
(LET T_64t2_105_4 =
                     ((((BVMOD(64, temp_96_2,temp_98_3) << 32)[63:0])&
                      0hexffffffff00000000)|
                     (BVDIV(64, temp_96_2,temp_98_3)&​0hex00000000ffffffff)) IN
(LET T_32t6_106_5 = T_64t2_105_4[31:0] IN
(LET final_EAX_112_6 = T_32t6_106_5 IN
IF (NOT(final_EAX_112_6=
BVDIV(32, initial_EAX_83_1,initial_EBX_​82_0))) THEN 0bin1 ELSE 0bin0 ENDIF)))))))
);
QUERY(FALSE);
COUNTEREXAMPLE;