⊟
17.7 KB
/srv/reproducible-results/rbuild-debian/r-b-build.cNiX0tLF/b1/cvc4_1.8-3_amd64.changes vs.
/srv/reproducible-results/rbuild-debian/r-b-build.cNiX0tLF/b2/cvc4_1.8-3_amd64.changes
⊟
1.21 KB
Files
    
Offset 1, 8 lines modifiedOffset 1, 8 lines modified
  
1 ·5a1c32ee62def72bddfdb0114f7e7c93·999176·debug·optional·cvc4-dbgsym_1.8-3_amd64.deb 
2 ·863b0df5ff608e42a2581037532a591e·82004·math·optional·cvc4_1.8-3_amd64.deb 
3 ·2d5bbb6b9f95eafe9a429811cae7c4c1·197458440·debug·optional·libcvc4-7-dbgsym_1.8-3_amd64.deb 
4 ·7146e0e17220f84461f75c9b6b669335·5993532·libs·optional·libcvc4-7_1.8-3_amd64.deb 
5 ·982e1ec0df8250df960cfa0c2233bee4·131188·libdevel·optional·libcvc4-dev_1.8-3_amd64.deb 
6 ·260879522b8cf68f90b61654503e63b1·5175588·debug·optional·libcvc4parser7-dbgsym_1.8-3_amd64.deb 
7 ·47287db7fa7ca12e45804c88820bc644·363964·libs·optional·libcvc4parser7_1.8-3_amd64.deb1 ·2e87c1f32359c0ef4d0a40fffccc5f82·999120·debug·optional·cvc4-dbgsym_1.8-3_amd64.deb
 2 ·c2b046d30699ca291c5914644b434c3b·81856·math·optional·cvc4_1.8-3_amd64.deb
 3 ·9ef5345ecbc141b280670f3c913ca8de·197452820·debug·optional·libcvc4-7-dbgsym_1.8-3_amd64.deb
 4 ·a62a3324f78551efbabb1021cc671abd·5997004·libs·optional·libcvc4-7_1.8-3_amd64.deb
 5 ·882302596967c6187f848d02da727a54·131176·libdevel·optional·libcvc4-dev_1.8-3_amd64.deb
 6 ·718445a51069d60f6288a46f40309082·5176340·debug·optional·libcvc4parser7-dbgsym_1.8-3_amd64.deb
 7 ·026fada2edfdd3c8b8f9f6133f0001f7·364232·libs·optional·libcvc4parser7_1.8-3_amd64.deb
⊟
7.39 KB
cvc4_1.8-3_amd64.deb
⊟
367 B
file list
    
Offset 1, 3 lines modifiedOffset 1, 3 lines modified
1 -rw-r--r--···0········0········0········4·2022-10-29·18:49:40.000000·debian-binary1 -rw-r--r--···0········0········0········4·2022-10-29·18:49:40.000000·debian-binary
2 -rw-r--r--···0········0········0·····1476·2022-10-29·18:49:40.000000·control.tar.xz2 -rw-r--r--···0········0········0·····1476·2022-10-29·18:49:40.000000·control.tar.xz
3 -rw-r--r--···0········0········0····80336·2022-10-29·18:49:40.000000·data.tar.xz3 -rw-r--r--···0········0········0····80188·2022-10-29·18:49:40.000000·data.tar.xz
⊟
98.0 B
control.tar.xz
⊟
70.0 B
control.tar
⊟
48.0 B
./md5sums
⊟
30.0 B
./md5sums
Files differ
⊟
6.9 KB
data.tar.xz
⊟
6.87 KB
data.tar
⊟
1.04 KB
file list
    
Offset 24, 8 lines modifiedOffset 24, 8 lines modified
24 -rw-r--r--···0·root·········(0)·root·········(0)·····2085·2020-06-19·16:59:27.000000·./usr/share/doc/cvc4/THANKS24 -rw-r--r--···0·root·········(0)·root·········(0)·····2085·2020-06-19·16:59:27.000000·./usr/share/doc/cvc4/THANKS
25 -rw-r--r--···0·root·········(0)·root·········(0)·····1043·2022-10-29·18:49:40.000000·./usr/share/doc/cvc4/changelog.Debian.gz25 -rw-r--r--···0·root·········(0)·root·········(0)·····1043·2022-10-29·18:49:40.000000·./usr/share/doc/cvc4/changelog.Debian.gz
26 -rw-r--r--···0·root·········(0)·root·········(0)·····4452·2022-10-17·14:15:49.000000·./usr/share/doc/cvc4/copyright26 -rw-r--r--···0·root·········(0)·root·········(0)·····4452·2022-10-17·14:15:49.000000·./usr/share/doc/cvc4/copyright
27 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/27 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/
28 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/man1/28 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/man1/
29 -rw-r--r--···0·root·········(0)·root·········(0)·····2116·2022-10-29·18:49:40.000000·./usr/share/man/man1/cvc4.1.gz29 -rw-r--r--···0·root·········(0)·root·········(0)·····2116·2022-10-29·18:49:40.000000·./usr/share/man/man1/cvc4.1.gz
30 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/man5/30 drwxr-xr-x···0·root·········(0)·root·········(0)········0·2022-10-29·18:49:40.000000·./usr/share/man/man5/
31 -rw-r--r--···0·root·········(0)·root·········(0)······394·2022-10-29·18:49:40.000000·./usr/share/man/man5/cvc4.5.gz31 -rw-r--r--···0·root·········(0)·root·········(0)······393·2022-10-29·18:49:40.000000·./usr/share/man/man5/cvc4.5.gz
⊟
4.91 KB
./usr/bin/cvc4
File has been modified after NT_GNU_BUILD_ID has been applied.
⊟
1.48 KB
readelf --wide --sections {}
    
Offset 4, 15 lines modifiedOffset 4, 15 lines modified
4 ··[Nr]·Name··············Type············Address··········Off····Size···ES·Flg·Lk·Inf·Al4 ··[Nr]·Name··············Type············Address··········Off····Size···ES·Flg·Lk·Inf·Al
5 ··[·0]···················NULL············0000000000000000·000000·000000·00······0···0··05 ··[·0]···················NULL············0000000000000000·000000·000000·00······0···0··0
6 ··[·1]·.interp···········PROGBITS········00000000000002a8·0002a8·00001c·00···A··0···0··16 ··[·1]·.interp···········PROGBITS········00000000000002a8·0002a8·00001c·00···A··0···0··1
7 ··[·2]·.note.gnu.property·NOTE············00000000000002c8·0002c8·000020·00···A··0···0··87 ··[·2]·.note.gnu.property·NOTE············00000000000002c8·0002c8·000020·00···A··0···0··8
8 ··[·3]·.note.ABI-tag·····NOTE············00000000000002e8·0002e8·000020·00···A··0···0··48 ··[·3]·.note.ABI-tag·····NOTE············00000000000002e8·0002e8·000020·00···A··0···0··4
9 ··[·4]·.note.gnu.build-id·NOTE············0000000000000308·000308·000024·00···A··0···0··49 ··[·4]·.note.gnu.build-id·NOTE············0000000000000308·000308·000024·00···A··0···0··4
10 ··[·5]·.dynsym···········DYNSYM··········0000000000000330·000330·002b98·18···A··6···1··810 ··[·5]·.dynsym···········DYNSYM··········0000000000000330·000330·002b98·18···A··6···1··8
11 ··[·6]·.dynstr···········STRTAB··········0000000000002ec8·002ec8·004cba·00···A··0···0··111 ··[·6]·.dynstr···········STRTAB··········0000000000002ec8·002ec8·004cbe·00···A··0···0··1
12 ··[·7]·.gnu.hash·········GNU_HASH········0000000000007b88·007b88·000778·00···A··5···0··812 ··[·7]·.gnu.hash·········GNU_HASH········0000000000007b88·007b88·000778·00···A··5···0··8
13 ··[·8]·.gnu.version······VERSYM··········0000000000008300·008300·0003a2·02···A··5···0··213 ··[·8]·.gnu.version······VERSYM··········0000000000008300·008300·0003a2·02···A··5···0··2
14 ··[·9]·.gnu.version_r····VERNEED·········00000000000086a4·0086a4·000110·00···A··6···4··414 ··[·9]·.gnu.version_r····VERNEED·········00000000000086a4·0086a4·000110·00···A··6···4··4
15 ··[10]·.rela.dyn·········RELA············00000000000087b8·0087b8·001290·18···A··5···0··815 ··[10]·.rela.dyn·········RELA············00000000000087b8·0087b8·001290·18···A··5···0··8
16 ··[11]·.rela.plt·········RELA············0000000000009a48·009a48·001488·18··AI··5··27··816 ··[11]·.rela.plt·········RELA············0000000000009a48·009a48·001488·18··AI··5··27··8
17 ··[12]·.init·············PROGBITS········000000000000aed0·00aed0·000017·00··AX··0···0··417 ··[12]·.init·············PROGBITS········000000000000aed0·00aed0·000017·00··AX··0···0··4
18 ··[13]·.plt··············PROGBITS········000000000000aef0·00aef0·000dc0·10··AX··0···0·1618 ··[13]·.plt··············PROGBITS········000000000000aef0·00aef0·000dc0·10··AX··0···0·16
⊟
1.01 KB
readelf --wide --dynamic {}
    
Offset 9, 15 lines modifiedOffset 9, 15 lines modified
9 ·0x0000000000000008·(RELASZ)·············4752·(bytes)9 ·0x0000000000000008·(RELASZ)·············4752·(bytes)
10 ·0x0000000000000009·(RELAENT)············24·(bytes)10 ·0x0000000000000009·(RELAENT)············24·(bytes)
11 ·0x000000006ffffff9·(RELACOUNT)··········10911 ·0x000000006ffffff9·(RELACOUNT)··········109
12 ·0x0000000000000015·(DEBUG)··············0x012 ·0x0000000000000015·(DEBUG)··············0x0
13 ·0x0000000000000006·(SYMTAB)·············0x33013 ·0x0000000000000006·(SYMTAB)·············0x330
14 ·0x000000000000000b·(SYMENT)·············24·(bytes)14 ·0x000000000000000b·(SYMENT)·············24·(bytes)
15 ·0x0000000000000005·(STRTAB)·············0x2ec815 ·0x0000000000000005·(STRTAB)·············0x2ec8
16 ·0x000000000000000a·(STRSZ)··············19642·(bytes)16 ·0x000000000000000a·(STRSZ)··············19646·(bytes)
17 ·0x000000006ffffef5·(GNU_HASH)···········0x7b8817 ·0x000000006ffffef5·(GNU_HASH)···········0x7b88
18 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcvc4parser.so.7]18 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcvc4parser.so.7]
19 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libreadline.so.8]19 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libreadline.so.8]
20 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcvc4.so.7]20 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcvc4.so.7]
21 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcln.so.6]21 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libcln.so.6]
22 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libstdc++.so.6]22 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libstdc++.so.6]
23 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libgcc_s.so.1]23 ·0x0000000000000001·(NEEDED)·············Shared·library:·[libgcc_s.so.1]
⊟
810 B
readelf --wide --notes {}
    
Offset 5, 12 lines modifiedOffset 5, 12 lines modified
  
5 Displaying·notes·found·in:·.note.ABI-tag5 Displaying·notes·found·in:·.note.ABI-tag
6 ··Owner················Data·size·»  Description6 ··Owner················Data·size·»  Description
7 ··GNU··················0x00000010»  NT_GNU_ABI_TAG·(ABI·version·tag)»     ····OS:·Linux,·ABI:·3.2.07 ··GNU··················0x00000010»  NT_GNU_ABI_TAG·(ABI·version·tag)»     ····OS:·Linux,·ABI:·3.2.0
  
8 Displaying·notes·found·in:·.note.gnu.build-id8 Displaying·notes·found·in:·.note.gnu.build-id
9 ··Owner················Data·size·»  Description9 ··Owner················Data·size·»  Description
10 ··GNU··················0x00000014»  NT_GNU_BUILD_ID·(unique·build·ID·bitstring)»   ····Build·ID:·b34c6d29179928c961d5e6ae803f3543729df79e10 ··GNU··················0x00000014»  NT_GNU_BUILD_ID·(unique·build·ID·bitstring)»   ····Build·ID:·d77270ec638e71974e21c104354986124d8f914a
  
11 Displaying·notes·found·in:·.note.gnu.gold-version11 Displaying·notes·found·in:·.note.gnu.gold-version
12 ··Owner················Data·size·»  Description12 ··Owner················Data·size·»  Description
13 ··GNU··················0x00000009»  NT_GNU_GOLD_VERSION·(gold·version)»  ····Version:·gold·1.1613 ··GNU··················0x00000009»  NT_GNU_GOLD_VERSION·(gold·version)»  ····Version:·gold·1.16
⊟
717 B
readelf --wide --decompress --hex-dump=.dynstr {}
    
Offset 1223, 9 lines modifiedOffset 1223, 9 lines modified
1223 ··0x00007b08·69626376·63342e73·6f2e3700·6c696263·ibcvc4.so.7.libc1223 ··0x00007b08·69626376·63342e73·6f2e3700·6c696263·ibcvc4.so.7.libc
1224 ··0x00007b18·6c6e2e73·6f2e3600·00000000·00000000·ln.so.6.........1224 ··0x00007b18·6c6e2e73·6f2e3600·00000000·00000000·ln.so.6.........
1225 ··0x00007b28·00000000·00000000·00000000·00000000·................1225 ··0x00007b28·00000000·00000000·00000000·00000000·................
1226 ··0x00007b38·00000000·00000000·00000000·00000000·................1226 ··0x00007b38·00000000·00000000·00000000·00000000·................
1227 ··0x00007b48·00000000·00000000·00000000·00000000·................1227 ··0x00007b48·00000000·00000000·00000000·00000000·................
1228 ··0x00007b58·00000000·00000000·00000000·00000000·................1228 ··0x00007b58·00000000·00000000·00000000·00000000·................
1229 ··0x00007b68·00000000·00000000·00000000·00000000·................1229 ··0x00007b68·00000000·00000000·00000000·00000000·................
1230 ··0x00007b78·00000000·00000000·0000··············..........1230 ··0x00007b78·00000000·00000000·00000000·0000·····..............
  
⊟
866 B
readelf --wide --decompress --hex-dump=.gnu_debuglink {}
error from `readelf --wide --decompress --hex-dump=.gnu_debuglink {}`: readelf: Error: Unable to find program interpreter name readelf: Error: no .dynamic section in the dynamic segment
    
Offset 1, 7 lines modifiedOffset 1, 7 lines modified
  
1 Hex·dump·of·section·'.gnu_debuglink':1 Hex·dump·of·section·'.gnu_debuglink':
2 ··0x00000000·34633664·32393137·39393238·63393631·4c6d29179928c961 
3 ··0x00000010·64356536·61653830·33663335·34333732·d5e6ae803f3543722 ··0x00000000·37323730·65633633·38653731·39373465·7270ec638e71974e
 3 ··0x00000010·32316331·30343335·34393836·31323464·21c104354986124d
4 ··0x00000020·39646637·39652e64·65627567·00000000·9df79e.debug....4 ··0x00000020·38663931·34612e64·65627567·00000000·8f914a.debug....
5 ··0x00000030·bdc2a120····························...·5 ··0x00000030·9c35e6b9····························.5..
  
⊟
412 B
./usr/share/man/man1/cvc4.1.gz
⊟
352 B
cvc4.1
    
Offset 1, 11 lines modifiedOffset 1, 11 lines modified
1 .\"·Process·this·file·with1 .\"·Process·this·file·with
2 .\"·groff·-man·-Tascii·cvc4.12 .\"·groff·-man·-Tascii·cvc4.1
3 .\"3 .\"
4 .TH·CVC4·1·"2022-10-29"·"CVC4·release·CVC4_RELEASE_STRING"·"User·Manuals"4 .TH·CVC4·1·"2022-10-30"·"CVC4·release·CVC4_RELEASE_STRING"·"User·Manuals"
5 .SH·NAME5 .SH·NAME
6 cvc4,·pcvc4·\-·an·automated·theorem·prover6 cvc4,·pcvc4·\-·an·automated·theorem·prover
7 .SH·SYNOPSIS7 .SH·SYNOPSIS
8 .B·cvc4·[8 .B·cvc4·[
9 .I·options9 .I·options
10 .B·]·[10 .B·]·[
11 .I·file11 .I·file
⊟
515 B
./usr/share/man/man5/cvc4.5.gz
⊟
455 B
cvc4.5
    
Offset 1, 11 lines modifiedOffset 1, 11 lines modified
1 .\"·Process·this·file·with1 .\"·Process·this·file·with
2 .\"·groff·-man·-Tascii·cvc4.52 .\"·groff·-man·-Tascii·cvc4.5
3 .\"3 .\"
4 .TH·CVC4·5·"2022-10-29"·"CVC4·release·CVC4_RELEASE_STRING"·"Languages·documentation"4 .TH·CVC4·5·"2022-10-30"·"CVC4·release·CVC4_RELEASE_STRING"·"Languages·documentation"
5 .SH·NAME5 .SH·NAME
6 cvc4·\-·the·native·input·language·for·CVC46 cvc4·\-·the·native·input·language·for·CVC4
7 .SH·DESCRIPTION7 .SH·DESCRIPTION
8 .B·cvc48 .B·cvc4
9 is·an·automated·theorem·prover·for·first-order·formulas·with·respect9 is·an·automated·theorem·prover·for·first-order·formulas·with·respect
10 to·background·theories·of·interest.10 to·background·theories·of·interest.
  
⊟
8.37 KB
libcvc4-7_1.8-3_amd64.deb
⊟
452 B
file list
    
Offset 1, 3 lines modifiedOffset 1, 3 lines modified
1 -rw-r--r--···0········0········0········4·2022-10-29·18:49:40.000000·debian-binary1 -rw-r--r--···0········0········0········4·2022-10-29·18:49:40.000000·debian-binary
2 -rw-r--r--···0········0········0·····1216·2022-10-29·18:49:40.000000·control.tar.xz2 -rw-r--r--···0········0········0·····1212·2022-10-29·18:49:40.000000·control.tar.xz
3 -rw-r--r--···0········0········0··5992124·2022-10-29·18:49:40.000000·data.tar.xz3 -rw-r--r--···0········0········0··5995600·2022-10-29·18:49:40.000000·data.tar.xz
⊟
98.0 B
control.tar.xz
⊟
70.0 B
control.tar
⊟
48.0 B
./md5sums
⊟
30.0 B
./md5sums
Files differ
⊟
7.78 KB
data.tar.xz
⊟
7.76 KB
data.tar
⊟
7.75 KB
./usr/lib/x86_64-linux-gnu/libcvc4.so.7
File has been modified after NT_GNU_BUILD_ID has been applied.
⊟
623 B
readelf --wide --notes {}
    
Offset 1, 8 lines modifiedOffset 1, 8 lines modified
  
1 Displaying·notes·found·in:·.note.gnu.build-id1 Displaying·notes·found·in:·.note.gnu.build-id
2 ··Owner················Data·size·»  Description2 ··Owner················Data·size·»  Description
3 ··GNU··················0x00000014»  NT_GNU_BUILD_ID·(unique·build·ID·bitstring)»   ····Build·ID:·ecc706a5c056fed55f11b3ae612e0c7fc481ffea3 ··GNU··················0x00000014»  NT_GNU_BUILD_ID·(unique·build·ID·bitstring)»   ····Build·ID:·36248cd85a156071448f81bdc6a890d600ff4ff8
  
4 Displaying·notes·found·in:·.note.gnu.gold-version4 Displaying·notes·found·in:·.note.gnu.gold-version
5 ··Owner················Data·size·»  Description5 ··Owner················Data·size·»  Description
6 ··GNU··················0x00000009»  NT_GNU_GOLD_VERSION·(gold·version)»  ····Version:·gold·1.166 ··GNU··················0x00000009»  NT_GNU_GOLD_VERSION·(gold·version)»  ····Version:·gold·1.16
⊟
5.89 KB
strings --all --bytes=8 {}
    
Offset 44582, 15 lines modifiedOffset 44582, 15 lines modified
44582 theory::arith::iteMinMaxApplicatteConstantApplictheory::arith::attempt::searchTittempt::queueTimttempt::conflicttheory::arith::congruence::watchwatchedVariablesedVariableIsZeroedVariableIsNotZongruence::equalalsConstantCallsongruence::propaagateConstraintsongruence::confltheory::arith::ArithCongruenceMad::unatePropagatgateImplicationstheory::arith::dio::conflictCallh::dio::cutCalls::dio::conflictsio::conflictTimeh::dio::cutTimeris·an·integer·variable·created·by·the·dio·solverual::UpdateConflual::findConflicctOnTheQueueTimeual::simplexConfual::recentViolaViolationCatchesdual::searchTimedual::lastPivotstheory::arith::ppqueue::enqueuesqueue::enqueuesCqueuesCollectionqueue::enqueuesDqueue::enqueuesVeuesVarOrderModeollectionDuplicaarOrderModeDuplitheory::arith::FC::initialProcesC::UpdateConflic::FC::FoundUnsatth::FC::FoundSatrith::FC::MissedFC::ConstructionC::selectUpdateFpdateForDualLike::FC::lastPivotstheory::arith::utheory::arith::weakening::attempeakening::succesweakening::total:weakening::timetheory::arith::fh::forcing::time44582 theory::arith::iteMinMaxApplicatteConstantApplictheory::arith::attempt::searchTittempt::queueTimttempt::conflicttheory::arith::congruence::watchwatchedVariablesedVariableIsZeroedVariableIsNotZongruence::equalalsConstantCallsongruence::propaagateConstraintsongruence::confltheory::arith::ArithCongruenceMad::unatePropagatgateImplicationstheory::arith::dio::conflictCallh::dio::cutCalls::dio::conflictsio::conflictTimeh::dio::cutTimeris·an·integer·variable·created·by·the·dio·solverual::UpdateConflual::findConflicctOnTheQueueTimeual::simplexConfual::recentViolaViolationCatchesdual::searchTimedual::lastPivotstheory::arith::ppqueue::enqueuesqueue::enqueuesCqueuesCollectionqueue::enqueuesDqueue::enqueuesVeuesVarOrderModeollectionDuplicaarOrderModeDuplitheory::arith::FC::initialProcesC::UpdateConflic::FC::FoundUnsatth::FC::FoundSatrith::FC::MissedFC::ConstructionC::selectUpdateFpdateForDualLike::FC::lastPivotstheory::arith::utheory::arith::weakening::attempeakening::succesweakening::total:weakening::timetheory::arith::fh::forcing::time
44583 phase·shifted·trrigonometric·argnumber·of·shiftstheory::arith::SOI::initialProceOI::UpdateConfli:SOI::FoundUnsath::SOI::FoundSatith::SOI::MissedOI::ConfMin::num:SOI::HasToBeMinSOI::MaybeNotMinOI::ConstructionOI::Conflict::Mict::Minimization::SOI::selectSOI:SOI::lastPivots::ppRewriteTimeran·extensional·lemma·index·variable·from·the·thetheory·of·arraysskolem·for·compuuting·signaturesabstraction·function·for·bv·theotheory::bv::algebraic::NumCallsTbraic::NumSimpliSimplifiesToTrueimplifiesToFalseebraic::NumUnsatlgebraic::NumSatbraic::NumUnknowbraic::SolveTimebraic::UseHeuristheory::bv::BitblastSolver::NumC:NumCallsToChecklastSolver::NumTNumTimesLemmasBBtheory::bv::lazytheory::bv::CoreSolver::NumCallsSolver::SlicerEntheory::bv::inequality::NumCallsuality::SolveTimtheory::bv::slicslicer::NumNodeser::NumRepresentlicer::NumSplitslicer::NumMergeser::AverageFindDer::NumEqualitietheory::bv::AvgBvgBVConflictSizetheory::bv::NumSolveSubstitutiontheory::bv::solvtheory::bv::NumFumFullCheckCallstandardCheckCalltheory::bv::weightComputationTimtheory::bv::NumMMultSliceAppliedeated·by·the·theory·of·bitvectortheory::datatypeEagerProofGeneraA·boolean·variable·asserted·to·be·true·to·force··force·a·restart44583 phase·shifted·trrigonometric·argnumber·of·shiftstheory::arith::SOI::initialProceOI::UpdateConfli:SOI::FoundUnsath::SOI::FoundSatith::SOI::MissedOI::ConfMin::num:SOI::HasToBeMinSOI::MaybeNotMinOI::ConstructionOI::Conflict::Mict::Minimization::SOI::selectSOI:SOI::lastPivots::ppRewriteTimeran·extensional·lemma·index·variable·from·the·thetheory·of·arraysskolem·for·compuuting·signaturesabstraction·function·for·bv·theotheory::bv::algebraic::NumCallsTbraic::NumSimpliSimplifiesToTrueimplifiesToFalseebraic::NumUnsatlgebraic::NumSatbraic::NumUnknowbraic::SolveTimebraic::UseHeuristheory::bv::BitblastSolver::NumC:NumCallsToChecklastSolver::NumTNumTimesLemmasBBtheory::bv::lazytheory::bv::CoreSolver::NumCallsSolver::SlicerEntheory::bv::inequality::NumCallsuality::SolveTimtheory::bv::slicslicer::NumNodeser::NumRepresentlicer::NumSplitslicer::NumMergeser::AverageFindDer::NumEqualitietheory::bv::AvgBvgBVConflictSizetheory::bv::NumSolveSubstitutiontheory::bv::solvtheory::bv::NumFumFullCheckCallstandardCheckCalltheory::bv::weightComputationTimtheory::bv::NumMMultSliceAppliedeated·by·the·theory·of·bitvectortheory::datatypeEagerProofGeneraA·boolean·variable·asserted·to·be·true·to·force··force·a·restart
44584 floatingpoint_mant_max_zero_casefloatingpoint_mint_min_zero_casefloatingpoint_to_real_infinity_aity_and_NaN_casevariable·to·represent·disjoint·et·extract·regionfree·infinity·for·virtual·term·serm·substitutioninfinity·for·virtual·term·substifree·delta·for·virtual·term·subsdelta·for·virtual·term·substitutConjectureGenerawas·created·by·conjecture·ground·term·enumeratorinternal·op·for·dynamic_rewritersygus-rr-synth-iskolem·created·for·full-model·chop·for·full-model-model·checkingop·created·durinring·fun·def·fmfInstStrategyEnumInstantiate::Instantiations_TotaInstantiate::Dup::Duplicate_Instuplicate_Inst_Eqlicate_Inst_Entalicate_Inst_ModeQuantConflictFinind::Inst_Roundsd::Entailment_ChEPR·base·constancreated·during·sng·skolemizationg·pre-skolemizatsingle·invocatioCannot·get·synth·function:·reconstruction·to·syno·syntax·failed.cegis_unif_num_e44584 floatingpoint_mant_max_zero_casefloatingpoint_mint_min_zero_casefloatingpoint_to_real_infinity_aity_and_NaN_casevariable·to·represent·disjoint·et·extract·regionfree·infinity·for·virtual·term·serm·substitutioninfinity·for·virtual·term·substifree·delta·for·virtual·term·subsdelta·for·virtual·term·substitutConjectureGenerawas·created·by·conjecture·ground·term·enumeratorinternal·op·for·dynamic_rewritersygus-rr-synth-iskolem·created·for·full-model·chop·for·full-model-model·checkingop·created·durinring·fun·def·fmfInstStrategyEnumInstantiate::Instantiations_TotaInstantiate::Dup::Duplicate_Instuplicate_Inst_Eqlicate_Inst_Entalicate_Inst_ModeQuantConflictFinind::Inst_Roundsd::Entailment_ChEPR·base·constancreated·during·sng·skolemizationg·pre-skolemizatsingle·invocatioCannot·get·synth·function:·reconstruction·to·syno·syntax·failed.cegis_unif_num_e
44585 00010203040506070809101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949529394959697989944585 000102030405060708091011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495293949596979899
44586 miniscope-quant-SynthEngine::ceg:cegqi_lemmas_ceqi_lemmas_refine:cegqi_lemmas_siSynthConjecture:cture::solutions:filtered_soluti:candidate_rewrie_rewrites_printSygusEnumerator::enumTermsRewrit:enumTermsEvalExrator::enumTerms44586 miniscope-quant-SynthEngine::ceg:cegqi_lemmas_ceqi_lemmas_refine:cegqi_lemmas_siSynthConjecture:cture::solutions:filtered_soluti:candidate_rewrie_rewrites_printSygusEnumerator::enumTermsRewrit:enumTermsEvalExrator::enumTerms
44587 head·of·unif·evaevaluation·pointqe·for·non-ground·single·invocatqe·for·function·in·non-ground·siingle·invocationfor·sygus·invarivariance·testingtemplate·inferenference·argumentnce·rev·argumentis·a·termDb·fresb·fresh·variablepredicate·to·force·higher-order·purify·for·function·operator·teror·term·indexingTheoryQuantifiercardinality·bound·element·for·setheory::sets::eetheory::shared_tSharedTermsDatabconstant·created·during·sort·infg·sort·inferenceinjection·for·monotonicity·consttheory::strings:rings::checkRunsgs::strategyRunsings::inferences:cdSimplificatioings::reductions:regexpUnfoldingtrings::rewrites:conflictsEqEngi:conflictsEagerP::conflictsInfer:lemmasEagerPrep::lemmasCmiSplit:lemmasRegisterTgisterTermAtomicngs::lemmasInferstring·purify·sk44587 head·of·unif·evaevaluation·pointqe·for·non-ground·single·invocatqe·for·function·in·non-ground·siingle·invocationfor·sygus·invarivariance·testingtemplate·inferenference·argumentnce·rev·argumentis·a·termDb·fresb·fresh·variablepredicate·to·force·higher-order·purify·for·function·operator·teror·term·indexingTheoryQuantifiercardinality·bound·element·for·setheory::sets::eetheory::shared_tSharedTermsDatabconstant·created·during·sort·infg·sort·inferenceinjection·for·monotonicity·consttheory::strings:rings::checkRunsgs::strategyRunsings::inferences:cdSimplificatioings::reductions:regexpUnfoldingtrings::rewrites:conflictsEqEngi:conflictsEagerP::conflictsInfer:lemmasEagerPrep::lemmasCmiSplit:lemmasRegisterTgisterTermAtomicngs::lemmasInferstring·purify·sk
44588 THEORY_SAT_SOLVEShared·assertionmissed-t-conflictheory::quantifiuf_combined_cardCardinalityExtension::Clique_Consion::Clique_Lemsion::Split_Lemmsion::Disambiguauate_Term_Lemmassion::Totality_Lsion::Max_Model_is·a·cardinalityality·lemma·termenumeration·to·meet·negative·car·card·constraint44588 THEORY_SAT_SOLVEShared·assertionmissed-t-conflictheory::quantifiuf_combined_cardCardinalityExtension::Clique_Consion::Clique_Lemsion::Split_Lemmsion::Disambiguauate_Term_Lemmassion::Totality_Lsion::Max_Model_is·a·cardinalityality·lemma·termenumeration·to·meet·negative·car·card·constraint
44589 or·extensionalit2022-10-29·06:49this·expression·contains·an·element·of·unknown·type·(such·as·an·abstract·value);·its·type·cannot·be·computed·until·it·is·substitsubstituted·awayProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais·an·unresolved·selector·type·ptype·placeholderis·a·shared·seleis·a·constructorFilesystem·accesss·not·permittedError·in·option·option·parsing:·184467440737095544589 or·extensionalit2022-10-30·08:49this·expression·contains·an·element·of·unknown·type·(such·as·an·abstract·value);·its·type·cannot·be·computed·until·it·is·substitsubstituted·awayProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais·an·unresolved·selector·type·ptype·placeholderis·a·shared·seleis·a·constructorFilesystem·accesss·not·permittedError·in·option·option·parsing:·1844674407370955
44590 resource::Bitblaresource::BvEagevEagerAssertStepresource::BvPropvPropagationStepresource::BvSatCSatConflictsStepresource::CnfSteresource::Decisiresource::LemmaSresource::ParseSresource::Preproresource::Quantiresource::Restarresource::Rewritresource::SatCon:SatConflictStepresource::Theory:TheoryCheckStep44590 resource::Bitblaresource::BvEagevEagerAssertStepresource::BvPropvPropagationStepresource::BvSatCSatConflictsStepresource::CnfSteresource::Decisiresource::LemmaSresource::ParseSresource::Preproresource::Quantiresource::Restarresource::Rewritresource::SatCon:SatConflictStepresource::Theory:TheoryCheckStep
44591 is·a·skolem·variable·imported·from·another·ExprM44591 is·a·skolem·variable·imported·from·another·ExprM
44592 unknown·option·fn·for·--uf-ss:·`44592 unknown·option·fn·for·--uf-ss:·`
44593 Y@ffffff44593 Y@ffffff
44594 N4CVC47context10ContextObjE44594 N4CVC47context10ContextObjE
44595 N4CVC47context16ContextNotifyObjE44595 N4CVC47context16ContextNotifyObjE
44596 N4CVC47context6CDListINS_12NodeTemplateILb1EEENS0_14DefaultCleanUpIS3_EESaIS3_EEE44596 N4CVC47context6CDListINS_12NodeTemplateILb1EEENS0_14DefaultCleanUpIS3_EESaIS3_EEE
⊟
54.0 B
.text
Timeout exceeded; details may be incomplete.
⊟
54.0 B
.fini
Timeout exceeded; details may be incomplete.
⊟
58.0 B
.rodata
Timeout exceeded; details may be incomplete.
⊟
78.0 B
.gcc_except_table
Timeout exceeded; details may be incomplete.
⊟
62.0 B
.eh_frame
Timeout exceeded; details may be incomplete.
⊟
70.0 B
.eh_frame_hdr
Timeout exceeded; details may be incomplete.
⊟
54.0 B
.tbss
Timeout exceeded; details may be incomplete.
⊟
80.0 B
.data.rel.ro.local
Timeout exceeded; details may be incomplete.
⊟
66.0 B
.fini_array
Timeout exceeded; details may be incomplete.
⊟
66.0 B
.init_array
Timeout exceeded; details may be incomplete.
⊟
68.0 B
.data.rel.ro
Timeout exceeded; details may be incomplete.
⊟
52.0 B
.got
Timeout exceeded; details may be incomplete.
⊟
60.0 B
.got.plt
Timeout exceeded; details may be incomplete.
⊟
54.0 B
.data
Timeout exceeded; details may be incomplete.
⊟
74.0 B
.tm_clone_table
Timeout exceeded; details may be incomplete.
⊟
52.0 B
.bss
Timeout exceeded; details may be incomplete.
⊟
72.0 B
.gnu_debuglink
Timeout exceeded; details may be incomplete.
⊟
62.0 B
.shstrtab
Timeout exceeded; details may be incomplete.
⊟
98.0 B
libcvc4-dev_1.8-3_amd64.deb
Timeout exceeded; details may be incomplete.
⊟
104 B
libcvc4parser7_1.8-3_amd64.deb
Timeout exceeded; details may be incomplete.
⊟
98.0 B
cvc4-dbgsym_1.8-3_amd64.deb
Timeout exceeded; details may be incomplete.
⊟
108 B
libcvc4-7-dbgsym_1.8-3_amd64.deb
Timeout exceeded; details may be incomplete.
⊟
118 B
libcvc4parser7-dbgsym_1.8-3_amd64.deb
Timeout exceeded; details may be incomplete.
Generated by diffoscope 245