Commit f533a6edb312047cb3248521d893cae03c028803

Thomas de Grivel 2023-08-04T19:08:27

integer

diff --git a/libc3/tag.c b/libc3/tag.c
index a2940c4..1319d97 100644
--- a/libc3/tag.c
+++ b/libc3/tag.c
@@ -265,19 +265,19 @@ s_tag * tag_add (const s_tag *a, const s_tag *b, s_tag *dest)
       integer_clean(&tmp);
       return dest;
     case TAG_S8:
-      return tag_init_s32(dest, a->data.s64 + b->data.s8);
+      return tag_init_s64(dest, a->data.s64 + b->data.s8);
     case TAG_S16:
-      return tag_init_s32(dest, a->data.s64 + b->data.s16);
+      return tag_init_s64(dest, a->data.s64 + b->data.s16);
     case TAG_S32:
-      return tag_init_s32(dest, a->data.s64 + b->data.s32);
+      return tag_init_s64(dest, a->data.s64 + b->data.s32);
     case TAG_S64:
       return tag_init_s64(dest, a->data.s64 + b->data.s64);
     case TAG_U8:
-      return tag_init_s32(dest, a->data.s64 + b->data.u8);
+      return tag_init_s64(dest, a->data.s64 + b->data.u8);
     case TAG_U16:
-      return tag_init_s32(dest, a->data.s64 + b->data.u16);
+      return tag_init_s64(dest, a->data.s64 + b->data.u16);
     case TAG_U32:
-      return tag_init_s32(dest, a->data.s64 + b->data.u32);
+      return tag_init_s64(dest, a->data.s64 + b->data.u32);
     case TAG_U64:
       return tag_init_s64(dest, a->data.s64 + b->data.u64);
     default:
diff --git a/sources.mk b/sources.mk
index 1cd3385..af9785c 100644
--- a/sources.mk
+++ b/sources.mk
@@ -7,8 +7,8 @@ C3_CONFIGURES = \
 	ic3/update_sources \
 	libc3/configure \
 	libc3/update_sources \
-	libtommath/configure \
 	libtommath/update_sources \
+	libtommath/configure \
 	test/configure \
 	test/update_sources \
 	ucd2c/configure \
diff --git a/sources.sh b/sources.sh
index 6258f96..8ce6976 100644
--- a/sources.sh
+++ b/sources.sh
@@ -1,4 +1,4 @@
 # sources.sh generated by update_sources
-C3_CONFIGURES='c3c/configure c3s/configure c3s/update_sources ic3/configure ic3/update_sources libc3/configure libc3/update_sources libtommath/configure libtommath/update_sources test/configure test/update_sources ucd2c/configure '
+C3_CONFIGURES='c3c/configure c3s/configure c3s/update_sources ic3/configure ic3/update_sources libc3/configure libc3/update_sources libtommath/update_sources libtommath/configure test/configure test/update_sources ucd2c/configure '
 C3_MAKEFILES='c3c/Makefile c3s/Makefile ic3/Makefile libc3/Makefile libc3/gen.mk libtommath/Makefile test/Makefile ucd2c/Makefile '
 C3_C_SOURCES='c3c/c3c.c c3s/buf_readline.c c3s/c3s.c c3s/buf_readline.h ic3/ic3.c ic3/buf_linenoise.c ic3/buf_linenoise.h ic3/linenoise.c libc3/abs.c libc3/abs.h libc3/buf.c libc3/buf.h libc3/buf_inspect_s32.h libc3/buf_inspect_s64.c libc3/buf_inspect_s64.h libc3/buf_inspect_sw.c libc3/buf_inspect_sw.h libc3/buf_inspect_u8.c libc3/buf_inspect_u8.h libc3/buf_inspect_u16.c libc3/buf_parse_s8.c libc3/call.c libc3/arg.c libc3/arg.h libc3/buf_inspect_u16.h libc3/array.c libc3/array.h libc3/binding.c libc3/c3.c libc3/buf_inspect_u32.c libc3/buf_inspect_u32.h libc3/buf_inspect_u64.c libc3/buf_inspect_u64.h libc3/buf_inspect_u64_binary.c libc3/binding.h libc3/buf_inspect_u64_binary.h libc3/buf_inspect_u64_octal.c libc3/buf_inspect_u64_octal.h libc3/buf_inspect_u64_decimal.c libc3/buf_inspect_u64_decimal.h libc3/buf_inspect_u64_hexadecimal.c libc3/bool.c libc3/bool.h libc3/buf_file.c libc3/buf_file.h libc3/buf_inspect_u64_hexadecimal.h libc3/buf_inspect_uw.c libc3/buf_inspect_uw.h libc3/buf_parse_s16.c libc3/buf_parse_s16.h libc3/buf_parse_s32.c libc3/buf_parse_s32.h libc3/buf_parse_s64.c libc3/buf_parse_s64.h libc3/buf_parse_sw.c libc3/buf_parse_sw.h libc3/buf_parse_u8.c libc3/buf_parse_u8.h libc3/buf_parse_u16.c libc3/buf_parse_u16.h libc3/buf_parse_u32.c libc3/buf_inspect.h libc3/buf_parse_u32.h libc3/buf_parse.h libc3/buf_parse_c.c libc3/buf_save.c libc3/buf_parse_u64.c libc3/buf_parse_u64.h libc3/buf_parse_uw.c libc3/buf_parse_uw.h libc3/set__fact.c libc3/facts_spec_cursor.c libc3/set__fact.h libc3/set__tag.c libc3/set__tag.h libc3/set_cursor__fact.c libc3/set_cursor__fact.h libc3/set_cursor__tag.c libc3/set_cursor__tag.h libc3/set_item__fact.c libc3/set_item__fact.h libc3/buf_parse_c.h libc3/buf_save.h libc3/c3.h libc3/c_types.h libc3/call.h libc3/set_item__tag.c libc3/set_item__tag.h libc3/skiplist__fact.c libc3/skiplist__fact.h libc3/skiplist_node__fact.c libc3/skiplist_node__fact.h libc3/ceiling.c libc3/ceiling.h libc3/cfn.c libc3/cfn.h libc3/character.c libc3/character.h libc3/buf_inspect_u8_octal.h libc3/compare.c libc3/buf_inspect.c libc3/compare.h libc3/buf_parse.c libc3/env.c libc3/env.h libc3/facts.c libc3/facts.h libc3/hash.c libc3/ident.c libc3/operator.c libc3/operator.h libc3/buf_inspect_s8.c libc3/buf_inspect_s8.h libc3/sym.c libc3/buf_inspect_s16.c libc3/buf_inspect_s16.h libc3/buf_inspect_s32.c libc3/buf_parse_s8.h libc3/error.c libc3/error.h libc3/error_handler.c libc3/error_handler.h libc3/eval.c libc3/eval.h libc3/buf_inspect_u8_binary.h libc3/fact.c libc3/fact.h libc3/facts_cursor.c libc3/facts_cursor.h libc3/facts_spec.c libc3/facts_spec.h libc3/facts_spec_cursor.h libc3/facts_with.c libc3/facts_with.h libc3/facts_with_cursor.c libc3/facts_with_cursor.h libc3/float.h libc3/fn.c libc3/fn.h libc3/frame.c libc3/frame.h libc3/hash.h libc3/ident.h libc3/integer.c libc3/integer.h libc3/io.c libc3/io.h libc3/list.c libc3/list.h libc3/log.c libc3/log.h libc3/buf_inspect_s.h.in libc3/module.c libc3/str.c libc3/module.h libc3/buf_parse_u.c.in libc3/quote.c libc3/quote.h libc3/set.c.in libc3/set.h.in libc3/buf_inspect_s_base.h.in libc3/sha1.h libc3/set_cursor.c.in libc3/set_cursor.h.in libc3/set_item.c.in libc3/set_item.h.in libc3/sign.c libc3/sign.h libc3/skiplist.c.in libc3/skiplist.h.in libc3/type.h libc3/skiplist_node.c.in libc3/skiplist_node.h.in libc3/str.h libc3/types.h libc3/ucd.c libc3/sym.h libc3/tuple.c libc3/tuple.h libc3/type.c libc3/ucd.h libc3/buf_parse_s.c.in libc3/buf_parse_s.h.in libc3/buf_inspect_s.c.in libc3/tag.c libc3/buf_parse_u.h.in libc3/buf_inspect_s16_binary.c libc3/buf_inspect_s16_binary.h libc3/buf_inspect_s16_decimal.c libc3/buf_inspect_s_base.c.in libc3/buf_inspect_s16_decimal.h libc3/buf_inspect_u.c.in libc3/buf_inspect_u.h.in libc3/buf_inspect_s16_hexadecimal.c libc3/buf_inspect_s16_hexadecimal.h libc3/buf_inspect_s16_octal.c libc3/buf_inspect_s16_octal.h libc3/buf_inspect_s32_binary.c libc3/buf_inspect_s32_binary.h libc3/buf_inspect_s32_decimal.c libc3/buf_inspect_s32_decimal.h libc3/buf_inspect_s32_hexadecimal.c libc3/buf_inspect_s32_hexadecimal.h libc3/buf_inspect_s32_octal.c libc3/buf_inspect_s32_octal.h libc3/buf_inspect_s64_binary.c libc3/buf_inspect_u_base.c.in libc3/buf_inspect_u_base.h.in libc3/buf_inspect_s64_binary.h libc3/buf_inspect_s64_decimal.c libc3/buf_inspect_s64_decimal.h libc3/buf_inspect_s64_hexadecimal.c libc3/buf_inspect_s64_hexadecimal.h libc3/buf_inspect_s64_octal.c libc3/buf_inspect_s64_octal.h libc3/tag.h libc3/buf_inspect_s8_binary.c libc3/buf_inspect_s8_binary.h libc3/buf_inspect_s8_decimal.c libc3/buf_inspect_s8_decimal.h libc3/buf_inspect_s8_hexadecimal.c libc3/buf_inspect_s8_hexadecimal.h libc3/buf_inspect_s8_octal.c libc3/buf_inspect_s8_octal.h libc3/buf_inspect_sw_binary.c libc3/buf_inspect_sw_binary.h libc3/buf_inspect_sw_decimal.c libc3/buf_inspect_sw_decimal.h libc3/buf_inspect_sw_hexadecimal.c libc3/buf_inspect_sw_hexadecimal.h libc3/buf_inspect_sw_octal.c libc3/buf_inspect_sw_octal.h libc3/buf_inspect_u16_binary.c libc3/buf_inspect_u16_binary.h libc3/buf_inspect_u16_decimal.c libc3/buf_inspect_u16_decimal.h libc3/buf_inspect_u16_hexadecimal.c libc3/buf_inspect_u16_hexadecimal.h libc3/buf_inspect_u16_octal.c libc3/buf_inspect_u16_octal.h libc3/buf_inspect_u32_binary.c libc3/buf_inspect_u32_binary.h libc3/buf_inspect_u32_decimal.c libc3/buf_inspect_u32_decimal.h libc3/buf_inspect_u32_hexadecimal.c libc3/buf_inspect_u32_hexadecimal.h libc3/buf_inspect_u32_octal.c libc3/buf_inspect_u32_octal.h libc3/buf_inspect_uw_binary.c libc3/buf_inspect_uw_binary.h libc3/buf_inspect_uw_decimal.c libc3/buf_inspect_uw_decimal.h libc3/buf_inspect_uw_hexadecimal.c libc3/buf_inspect_uw_hexadecimal.h libc3/buf_inspect_uw_octal.c libc3/buf_inspect_uw_octal.h libc3/buf_inspect_u8_octal.c libc3/buf_inspect_u8_binary.c libc3/buf_inspect_u8_decimal.c libc3/buf_inspect_u8_decimal.h libc3/buf_inspect_u8_hexadecimal.c libc3/buf_inspect_u8_hexadecimal.h test/buf_inspect_test.c test/bool_test.c test/buf_parse_test.c test/facts_test.c test/buf_file_test.c test/libc3_test.c test/list_test.c test/test.c test/test.h test/buf_parse_test_u8.c test/buf_parse_test.h test/buf_parse_test_s16.c test/buf_parse_test_s32.c test/buf_parse_test_s64.c test/buf_parse_test_s8.c test/buf_parse_test_su.h test/buf_parse_test_u16.c test/buf_parse_test_u32.c test/buf_test.c test/buf_parse_test_u64.c test/call_test.c test/facts_cursor_test.c test/cfn_test.c test/character_test.c test/compare_test.c test/compare_test.h test/env_test.c test/fact_test.c test/fact_test.h test/facts_with_test.c test/hash_test.c test/ident_test.c test/set__fact_test.c test/set__tag_test.c test/skiplist__fact_test.c test/str_test.c test/sym_test.c test/tag_test.c test/tag_test.h test/tuple_test.c test/types_test.c ucd2c/ucd.h ucd2c/ucd2c.c '
diff --git a/test/ic3/integer.in b/test/ic3/integer.in
index c4630c4..bc445cf 100644
--- a/test/ic3/integer.in
+++ b/test/ic3/integer.in
@@ -82,6 +82,103 @@
 
 -1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
 
-1 + 2
-123456789012345678901234567890123456789012345678901234567890 + 1
-1 + 123456789012345678901234567890123456789012345678901234567890
+-18446744073709551616 + -18446744073709551616
+-18446744073709551616 + -4294967296
+-18446744073709551616 + -32769
+-18446744073709551616 + -129
+-18446744073709551616 + -1
+-18446744073709551616 + 1
+-18446744073709551616 + 256
+-18446744073709551616 + 65536
+-18446744073709551616 + 8589934592
+-18446744073709551616 + 36893488147419103232
+-4294967296 + -18446744073709551616
+-4294967296 + -4294967296
+-4294967296 + -32769
+-4294967296 + -129
+-4294967296 + -1
+-4294967296 + 1
+-4294967296 + 256
+-4294967296 + 65536
+-4294967296 + 8589934592
+-4294967296 + 36893488147419103232
+-32769 + -18446744073709551616
+-32769 + -4294967296
+-32769 + -32769
+-32769 + -129
+-32769 + -1
+-32769 + 1
+-32769 + 256
+-32769 + 65536
+-32769 + 8589934592
+-32769 + 36893488147419103232
+-129 + -18446744073709551616
+-129 + -4294967296
+-129 + -32769
+-129 + -129
+-129 + -1
+-129 + 1
+-129 + 256
+-129 + 65536
+-129 + 8589934592
+-129 + 36893488147419103232
+-1 + -18446744073709551616
+-1 + -4294967296
+-1 + -32769
+-1 + -129
+-1 + -1
+-1 + 1
+-1 + 256
+-1 + 65536
+-1 + 8589934592
+-1 + 36893488147419103232
+1 + -18446744073709551616
+1 + -4294967296
+1 + -32769
+1 + -129
+1 + -1
+1 + 1
+1 + 256
+1 + 65536
+1 + 8589934592
+1 + 36893488147419103232
+256 + -18446744073709551616
+256 + -4294967296
+256 + -32769
+256 + -257
+256 + -1
+256 + 1
+256 + 256
+256 + 65536
+256 + 8589934592
+256 + 36893488147419103232
+65536 + -18446744073709551616
+65536 + -4294967296
+65536 + -32769
+65536 + -129
+65536 + -1
+65536 + 1
+65536 + 256
+65536 + 65536
+65536 + 8589934592
+65536 + 36893488147419103232
+8589934592 + -18446744073709551616
+8589934592 + -4294967296
+8589934592 + -32769
+8589934592 + -129
+8589934592 + -1
+8589934592 + 1
+8589934592 + 256
+8589934592 + 65536
+8589934592 + 8589934592
+8589934592 + 36893488147419103232
+36893488147419103232 + -18446744073709551616
+36893488147419103232 + -4294967296
+36893488147419103232 + -32769
+36893488147419103232 + -129
+36893488147419103232 + -1
+36893488147419103232 + 1
+36893488147419103232 + 256
+36893488147419103232 + 65536
+36893488147419103232 + 8589934592
+36893488147419103232 + 36893488147419103232
diff --git a/test/ic3/integer.lisp b/test/ic3/integer.lisp
new file mode 100644
index 0000000..a8f07ab
--- /dev/null
+++ b/test/ic3/integer.lisp
@@ -0,0 +1,105 @@
+(in-package :cl-user)
+
+(with-open-file (out #P"~/integer.out"
+                     :direction :output
+                     :element-type 'character)
+  (format out "~A~%" (+ -18446744073709551616 -18446744073709551616))
+  (format out "~A~%" (+ -18446744073709551616 -4294967296))
+  (format out "~A~%" (+ -18446744073709551616 -32769))
+  (format out "~A~%" (+ -18446744073709551616 -129))
+  (format out "~A~%" (+ -18446744073709551616 -1))
+  (format out "~A~%" (+ -18446744073709551616 1))
+  (format out "~A~%" (+ -18446744073709551616 256))
+  (format out "~A~%" (+ -18446744073709551616 65536))
+  (format out "~A~%" (+ -18446744073709551616 8589934592))
+  (format out "~A~%" (+ -18446744073709551616 36893488147419103232))
+  (format out "~A~%" (+ -4294967296 -18446744073709551616))
+  (format out "~A~%" (+ -4294967296 -4294967296))
+  (format out "~A~%" (+ -4294967296 -32769))
+  (format out "~A~%" (+ -4294967296 -129))
+  (format out "~A~%" (+ -4294967296 -1))
+  (format out "~A~%" (+ -4294967296 1))
+  (format out "~A~%" (+ -4294967296 256))
+  (format out "~A~%" (+ -4294967296 65536))
+  (format out "~A~%" (+ -4294967296 8589934592))
+  (format out "~A~%" (+ -4294967296 36893488147419103232))
+  (format out "~A~%" (+ -32769 -18446744073709551616))
+  (format out "~A~%" (+ -32769 -4294967296))
+  (format out "~A~%" (+ -32769 -32769))
+  (format out "~A~%" (+ -32769 -129))
+  (format out "~A~%" (+ -32769 -1))
+  (format out "~A~%" (+ -32769 1))
+  (format out "~A~%" (+ -32769 256))
+  (format out "~A~%" (+ -32769 65536))
+  (format out "~A~%" (+ -32769 8589934592))
+  (format out "~A~%" (+ -32769 36893488147419103232))
+  (format out "~A~%" (+ -129 -18446744073709551616))
+  (format out "~A~%" (+ -129 -4294967296))
+  (format out "~A~%" (+ -129 -32769))
+  (format out "~A~%" (+ -129 -129))
+  (format out "~A~%" (+ -129 -1))
+  (format out "~A~%" (+ -129 1))
+  (format out "~A~%" (+ -129 256))
+  (format out "~A~%" (+ -129 65536))
+  (format out "~A~%" (+ -129 8589934592))
+  (format out "~A~%" (+ -129 36893488147419103232))
+  (format out "~A~%" (+ -1 -18446744073709551616))
+  (format out "~A~%" (+ -1 -4294967296))
+  (format out "~A~%" (+ -1 -32769))
+  (format out "~A~%" (+ -1 -129))
+  (format out "~A~%" (+ -1 -1))
+  (format out "~A~%" (+ -1 1))
+  (format out "~A~%" (+ -1 256))
+  (format out "~A~%" (+ -1 65536))
+  (format out "~A~%" (+ -1 8589934592))
+  (format out "~A~%" (+ -1 36893488147419103232))
+  (format out "~A~%" (+ 1 -18446744073709551616))
+  (format out "~A~%" (+ 1 -4294967296))
+  (format out "~A~%" (+ 1 -32769))
+  (format out "~A~%" (+ 1 -129))
+  (format out "~A~%" (+ 1 -1))
+  (format out "~A~%" (+ 1 1))
+  (format out "~A~%" (+ 1 256))
+  (format out "~A~%" (+ 1 65536))
+  (format out "~A~%" (+ 1 8589934592))
+  (format out "~A~%" (+ 1 36893488147419103232))
+  (format out "~A~%" (+ 256 -18446744073709551616))
+  (format out "~A~%" (+ 256 -4294967296))
+  (format out "~A~%" (+ 256 -32769))
+  (format out "~A~%" (+ 256 -257))
+  (format out "~A~%" (+ 256 -1))
+  (format out "~A~%" (+ 256 1))
+  (format out "~A~%" (+ 256 256))
+  (format out "~A~%" (+ 256 65536))
+  (format out "~A~%" (+ 256 8589934592))
+  (format out "~A~%" (+ 256 36893488147419103232))
+  (format out "~A~%" (+ 65536 -18446744073709551616))
+  (format out "~A~%" (+ 65536 -4294967296))
+  (format out "~A~%" (+ 65536 -32769))
+  (format out "~A~%" (+ 65536 -129))
+  (format out "~A~%" (+ 65536 -1))
+  (format out "~A~%" (+ 65536 1))
+  (format out "~A~%" (+ 65536 256))
+  (format out "~A~%" (+ 65536 65536))
+  (format out "~A~%" (+ 65536 8589934592))
+  (format out "~A~%" (+ 65536 36893488147419103232))
+  (format out "~A~%" (+ 8589934592 -18446744073709551616))
+  (format out "~A~%" (+ 8589934592 -4294967296))
+  (format out "~A~%" (+ 8589934592 -32769))
+  (format out "~A~%" (+ 8589934592 -129))
+  (format out "~A~%" (+ 8589934592 -1))
+  (format out "~A~%" (+ 8589934592 1))
+  (format out "~A~%" (+ 8589934592 256))
+  (format out "~A~%" (+ 8589934592 65536))
+  (format out "~A~%" (+ 8589934592 8589934592))
+  (format out "~A~%" (+ 8589934592 36893488147419103232))
+  (format out "~A~%" (+ 36893488147419103232 -18446744073709551616))
+  (format out "~A~%" (+ 36893488147419103232 -4294967296))
+  (format out "~A~%" (+ 36893488147419103232 -32769))
+  (format out "~A~%" (+ 36893488147419103232 -129))
+  (format out "~A~%" (+ 36893488147419103232 -1))
+  (format out "~A~%" (+ 36893488147419103232 1))
+  (format out "~A~%" (+ 36893488147419103232 256))
+  (format out "~A~%" (+ 36893488147419103232 65536))
+  (format out "~A~%" (+ 36893488147419103232 8589934592))
+  (format out "~A~%" (+ 36893488147419103232 36893488147419103232)))
diff --git a/test/ic3/integer.out.expected b/test/ic3/integer.out.expected
index 73643b4..7bad384 100644
--- a/test/ic3/integer.out.expected
+++ b/test/ic3/integer.out.expected
@@ -68,6 +68,103 @@
 -1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
 -1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
-3
-123456789012345678901234567890123456789012345678901234567891
-123456789012345678901234567890123456789012345678901234567891
+-36893488147419103232
+-18446744078004518912
+-18446744073709584385
+-18446744073709551745
+-18446744073709551617
+-18446744073709551615
+-18446744073709551360
+-18446744073709486080
+-18446744065119617024
+18446744073709551616
+-18446744078004518912
+-8589934592
+-4295000065
+-4294967425
+-4294967297
+-4294967295
+-4294967040
+-4294901760
+4294967296
+36893488143124135936
+-18446744073709584385
+-4295000065
+-65538
+-32898
+-32770
+-32768
+-32513
+32767
+8589901823
+36893488147419070463
+-18446744073709551745
+-4294967425
+-32898
+-258
+-130
+-128
+127
+65407
+8589934463
+36893488147419103103
+-18446744073709551617
+-4294967297
+-32770
+-130
+-2
+0
+255
+65535
+8589934591
+36893488147419103231
+-18446744073709551615
+-4294967295
+-32768
+-128
+0
+2
+257
+65537
+8589934593
+36893488147419103233
+-18446744073709551360
+-4294967040
+-32513
+-1
+255
+257
+512
+65792
+8589934848
+36893488147419103488
+-18446744073709486080
+-4294901760
+32767
+65407
+65535
+65537
+65792
+131072
+8590000128
+36893488147419168768
+-18446744065119617024
+4294967296
+8589901823
+8589934463
+8589934591
+8589934593
+8589934848
+8590000128
+17179869184
+36893488156009037824
+18446744073709551616
+36893488143124135936
+36893488147419070463
+36893488147419103103
+36893488147419103231
+36893488147419103233
+36893488147419103488
+36893488147419168768
+36893488156009037824
+73786976294838206464