diff --git a/src/bignum.c b/src/bignum.c
index 19581433c0c06245c04e5601668f794256a25347..325a4dd1754c3aeaae799c403dca0aa671ef1ff3 100644
--- a/src/bignum.c
+++ b/src/bignum.c
@@ -150,6 +150,9 @@ PMOD_EXPORT void push_int64(INT64 i)
       i = -i;
       neg = 1;
     }
+
+    resolve_auto_bignum_program();
+
 #if PIKE_BYTEORDER == 1234
     {
       char digits[8];