execve("/opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4_real", ["/opt/Isabelle2016-1-RC1/contrib/"..., "--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--random-seed=1", "--lang=smt2", "--continued-execution", "--tlimit", "5757", "/tmp/isabelle-gene/process397010"...], [/* 176 vars */]) = 0 uname({sysname="Linux", nodename="home.starkeffect.com", ...}) = 0 brk(NULL) = 0x2cd3000 brk(0x2cd41c0) = 0x2cd41c0 arch_prctl(ARCH_SET_FS, 0x2cd3880) = 0 brk(0x2cf51c0) = 0x2cf51c0 brk(0x2cf6000) = 0x2cf6000 gettimeofday({1478265799, 105987}, NULL) = 0 getpid() = 14765 mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f7253000 gettimeofday({1478265799, 106208}, NULL) = 0 clock_gettime(CLOCK_MONOTONIC, {574344, 268960906}) = 0 brk(0x2d18000) = 0x2d18000 sigaltstack({ss_sp=0x2cf5ac0, ss_flags=0, ss_size=8192}, NULL) = 0 getrlimit(RLIMIT_STACK, {rlim_cur=8192*1024, rlim_max=RLIM64_INFINITY}) = 0 setrlimit(RLIMIT_STACK, {rlim_cur=RLIM64_INFINITY, rlim_max=RLIM64_INFINITY}) = 0 getrlimit(RLIMIT_STACK, {rlim_cur=RLIM64_INFINITY, rlim_max=RLIM64_INFINITY}) = 0 rt_sigaction(SIGINT, {0x431ff0, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0 rt_sigaction(SIGXCPU, {0x431f90, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0 rt_sigaction(SIGSEGV, {0x432050, [], SA_RESTORER|SA_STACK|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0 rt_sigaction(SIGILL, {0x432050, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0 gettimeofday({1478265799, 106439}, NULL) = 0 brk(0x2d39000) = 0x2d39000 brk(0x2d5d000) = 0x2d5d000 brk(0x2d81000) = 0x2d81000 brk(0x2da7000) = 0x2da7000 brk(0x2dd3000) = 0x2dd3000 mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f6e12000 mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f69d1000 brk(0x2df5000) = 0x2df5000 brk(0x2e17000) = 0x2e17000 brk(0x2e4d000) = 0x2e4d000 brk(0x2e77000) = 0x2e77000 brk(0x2e98000) = 0x2e98000 brk(0x2eb9000) = 0x2eb9000 brk(0x2eda000) = 0x2eda000 open("/tmp/isabelle-gene/process3970109973954785755/cache-io-31231432", O_RDONLY) = 4 stat("/tmp/isabelle-gene/process3970109973954785755/cache-io-31231432", {st_mode=S_IFREG|0664, st_size=67267, ...}) = 0 fstat(4, {st_mode=S_IFREG|0664, st_size=67267, ...}) = 0 mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f69d0000 read(4, "; --full-saturate-quant --inst-w"..., 65536) = 65536 read(4, "omp$ (pair$ (fun_app$ ?v6 (comp$"..., 4096) = 1731 close(4) = 0 munmap(0x7fc3f69d0000, 4096) = 0 mmap(NULL, 274432, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f698e000 munmap(0x7fc3f698e000, 274432) = 0 brk(0x2efb000) = 0x2efb000 gettimeofday({1478265799, 107688}, NULL) = 0 gettimeofday({1478265799, 107725}, NULL) = 0 gettimeofday({1478265799, 107743}, NULL) = 0 gettimeofday({1478265799, 107759}, NULL) = 0 gettimeofday({1478265799, 107775}, NULL) = 0 gettimeofday({1478265799, 107793}, NULL) = 0 gettimeofday({1478265799, 107810}, NULL) = 0 gettimeofday({1478265799, 107826}, NULL) = 0 gettimeofday({1478265799, 107843}, NULL) = 0 gettimeofday({1478265799, 107859}, NULL) = 0 ... gettimeofday({1478265799, 151033}, NULL) = 0 gettimeofday({1478265799, 151150}, NULL) = 0 brk(0x306c000) = 0x306c000 gettimeofday({1478265799, 151195}, NULL) = 0 gettimeofday({1478265799, 151319}, NULL) = 0 gettimeofday({1478265799, 151351}, NULL) = 0 gettimeofday({1478265799, 151663}, NULL) = 0 gettimeofday({1478265799, 151702}, NULL) = 0 gettimeofday({1478265799, 152005}, NULL) = 0 gettimeofday({1478265799, 152042}, NULL) = 0 gettimeofday({1478265799, 152350}, NULL) = 0 gettimeofday({1478265799, 152388}, NULL) = 0 gettimeofday({1478265799, 152539}, NULL) = 0 gettimeofday({1478265799, 152568}, NULL) = 0 gettimeofday({1478265799, 152702}, NULL) = 0 gettimeofday({1478265799, 152733}, NULL) = 0 gettimeofday({1478265799, 152886}, NULL) = 0 gettimeofday({1478265799, 152917}, NULL) = 0 gettimeofday({1478265799, 153074}, NULL) = 0 gettimeofday({1478265799, 153104}, NULL) = 0 gettimeofday({1478265799, 153253}, NULL) = 0 gettimeofday({1478265799, 153321}, NULL) = 0 gettimeofday({1478265799, 153339}, NULL) = 0 gettimeofday({1478265799, 153351}, NULL) = 0 gettimeofday({1478265799, 153359}, NULL) = 0 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 clock_gettime(CLOCK_MONOTONIC, {574344, 316111956}) = 0 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 clock_gettime(CLOCK_MONOTONIC, {574344, 316130143}) = 0 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350 ... times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565 clock_gettime(CLOCK_MONOTONIC, {574346, 470405093}) = 0 brk(0x3e8d000) = 0x3e8d000 brk(0x3ebe000) = 0x3ebe000 brk(0x3eea000) = 0x3eea000 brk(0x3f10000) = 0x3f10000 brk(0x3f31000) = 0x3f31000 brk(0x3f54000) = 0x3f54000 brk(0x3f75000) = 0x3f75000 brk(0x3f96000) = 0x3f96000 brk(0x3fb9000) = 0x3fb9000 times({tms_utime=67, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391566 brk(0x3fda000) = 0x3fda000 brk(0x4000000) = 0x4000000 brk(0x4024000) = 0x4024000 brk(0x404c000) = 0x404c000 brk(0x4082000) = 0x4082000 brk(0x40c2000) = 0x40c2000 brk(0x40fa000) = 0x40fa000 brk(0x412a000) = 0x412a000 brk(0x414b000) = 0x414b000 brk(0x4170000) = 0x4170000 brk(0x4191000) = 0x4191000 brk(0x41d5000) = 0x41d5000 brk(0x41f9000) = 0x41f9000 brk(0x421a000) = 0x421a000 brk(0x423b000) = 0x423b000 brk(0x425f000) = 0x425f000 brk(0x4280000) = 0x4280000 brk(0x42a3000) = 0x42a3000 brk(0x42c4000) = 0x42c4000 brk(0x42e5000) = 0x42e5000 brk(0x431b000) = 0x431b000 brk(0x435b000) = 0x435b000 brk(0x4393000) = 0x4393000 brk(0x43b5000) = 0x43b5000 brk(0x43dd000) = 0x43dd000 brk(0x440d000) = 0x440d000 brk(0x448d000) = 0x448d000 brk(0x44cd000) = 0x44cd000 brk(0x44ee000) = 0x44ee000 brk(0x450f000) = 0x450f000 brk(0x4536000) = 0x4536000 brk(0x4557000) = 0x4557000 brk(0x4578000) = 0x4578000 brk(0x45c4000) = 0x45c4000 brk(0x460d000) = 0x460d000 brk(0x463f000) = 0x463f000 brk(0x4662000) = 0x4662000 brk(0x46d8000) = 0x46d8000 brk(0x4711000) = 0x4711000 brk(0x473f000) = 0x473f000 brk(0x4760000) = 0x4760000 brk(0x4781000) = 0x4781000 brk(0x47a2000) = 0x47a2000 brk(0x47ce000) = 0x47ce000 brk(0x47ef000) = 0x47ef000 brk(0x4824000) = 0x4824000 brk(0x4848000) = 0x4848000 brk(0x4887000) = 0x4887000 brk(0x48e7000) = 0x48e7000 brk(0x4937000) = 0x4937000 brk(0x4958000) = 0x4958000 brk(0x49c1000) = 0x49c1000 brk(0x4a01000) = 0x4a01000 mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f634c000 mmap(NULL, 528384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f62cb000 brk(0x4a24000) = 0x4a24000 brk(0x4a47000) = 0x4a47000 brk(0x4a8d000) = 0x4a8d000 times({tms_utime=74, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391574 brk(0x4aae000) = 0x4aae000 brk(0x4acf000) = 0x4acf000 brk(0x4af0000) = 0x4af0000 brk(0x4b11000) = 0x4b11000 brk(0x4b32000) = 0x4b32000 brk(0x4b53000) = 0x4b53000 brk(0x4b74000) = 0x4b74000 brk(0x4b95000) = 0x4b95000 brk(0x4bb6000) = 0x4bb6000 brk(0x4bd8000) = 0x4bd8000 brk(0x4bf9000) = 0x4bf9000 brk(0x4c1a000) = 0x4c1a000 brk(0x4c3b000) = 0x4c3b000 brk(0x4c7a000) = 0x4c7a000 brk(0x4c9b000) = 0x4c9b000 clock_gettime(CLOCK_MONOTONIC, {574346, 573323696}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 573339863}) = 0 times({tms_utime=76, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391576 brk(0x4cd9000) = 0x4cd9000 brk(0x4cfa000) = 0x4cfa000 brk(0x4d1b000) = 0x4d1b000 brk(0x4d3c000) = 0x4d3c000 brk(0x4d5d000) = 0x4d5d000 brk(0x4d81000) = 0x4d81000 brk(0x4da3000) = 0x4da3000 brk(0x4dc6000) = 0x4dc6000 brk(0x4de7000) = 0x4de7000 brk(0x4e08000) = 0x4e08000 brk(0x4e29000) = 0x4e29000 brk(0x4e4a000) = 0x4e4a000 brk(0x4e73000) = 0x4e73000 brk(0x4e95000) = 0x4e95000 brk(0x4ebe000) = 0x4ebe000 brk(0x4edf000) = 0x4edf000 brk(0x4f19000) = 0x4f19000 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 clock_gettime(CLOCK_MONOTONIC, {574346, 634706517}) = 0 brk(0x4f3a000) = 0x4f3a000 mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f620a000 brk(0x4f81000) = 0x4f81000 clock_gettime(CLOCK_MONOTONIC, {574346, 639091777}) = 0 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 clock_gettime(CLOCK_MONOTONIC, {574346, 639148374}) = 0 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 clock_gettime(CLOCK_MONOTONIC, {574346, 639505911}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 639524027}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 639534898}) = 0 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582 ... clock_gettime(CLOCK_MONOTONIC, {574346, 664332065}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664339639}) = 0 times({tms_utime=83, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391585 clock_gettime(CLOCK_MONOTONIC, {574346, 664355428}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664364971}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664373588}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664382285}) = 0 times({tms_utime=83, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391585 clock_gettime(CLOCK_MONOTONIC, {574346, 664398105}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664406825}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664414900}) = 0 clock_gettime(CLOCK_MONOTONIC, {574346, 664424158}) = 0 brk(0x5056000) = 0x5056000 brk(0x5077000) = 0x5077000 clock_gettime(CLOCK_MONOTONIC, {574346, 674643892}) = 0 brk(0x5099000) = 0x5099000 brk(0x50ba000) = 0x50ba000 brk(0x50db000) = 0x50db000 brk(0x50fc000) = 0x50fc000 brk(0x511d000) = 0x511d000 brk(0x513e000) = 0x513e000 brk(0x515f000) = 0x515f000 brk(0x5180000) = 0x5180000 brk(0x51a1000) = 0x51a1000 brk(0x51c2000) = 0x51c2000 brk(0x51e3000) = 0x51e3000 brk(0x5204000) = 0x5204000 brk(0x5225000) = 0x5225000 brk(0x5246000) = 0x5246000 brk(0x5267000) = 0x5267000 brk(0x5288000) = 0x5288000 brk(0x52a9000) = 0x52a9000 brk(0x52ca000) = 0x52ca000 brk(0x52eb000) = 0x52eb000 brk(0x530c000) = 0x530c000 brk(0x532d000) = 0x532d000 brk(0x534e000) = 0x534e000 brk(0x536f000) = 0x536f000 --- SIGINT {si_signo=SIGINT, si_code=SI_USER, si_pid=4567, si_uid=1000} --- write(2, "CVC4 interrupted by user.\n", 26) = 26 rt_sigprocmask(SIG_UNBLOCK, [ABRT], NULL, 8) = 0 tgkill(14765, 14765, SIGABRT) = 0 --- SIGABRT {si_signo=SIGABRT, si_code=SI_TKILL, si_pid=14765, si_uid=1000} --- +++ killed by SIGABRT (core dumped) +++