--- /srv/reproducible-results/rbuild-debian/tmp.jVXSMpVkOC/b1/cvc4_1.8-2_amd64.changes +++ /srv/reproducible-results/rbuild-debian/tmp.jVXSMpVkOC/b2/cvc4_1.8-2_amd64.changes ├── Files │ @@ -1,8 +1,8 @@ │ │ - 57f9e049671b4cfdec4badb270ecf67d 992796 debug optional cvc4-dbgsym_1.8-2_amd64.deb │ - ea0dd9f3ff049dcbf46e1b4f66cfb494 81592 math optional cvc4_1.8-2_amd64.deb │ - 5591d2b48273d819ffdc526f02c5be6b 186533948 debug optional libcvc4-7-dbgsym_1.8-2_amd64.deb │ - b7a31c6f42c0e0dd903ac74ee7593409 5647544 libs optional libcvc4-7_1.8-2_amd64.deb │ - 94293bbac04ae60de40cb3adc5ad4de6 131264 libdevel optional libcvc4-dev_1.8-2_amd64.deb │ - 090c4ecadd615a31a5af7877d7707935 5162036 debug optional libcvc4parser7-dbgsym_1.8-2_amd64.deb │ - e787c58d30c743407f048b8f9dd92ed2 365872 libs optional libcvc4parser7_1.8-2_amd64.deb │ + f6c6f9d6eb3788997d622e87c1b5b1a0 992872 debug optional cvc4-dbgsym_1.8-2_amd64.deb │ + dfc37fad3f189901988e83fec2185528 81644 math optional cvc4_1.8-2_amd64.deb │ + 38f09895549eed8c3e4df99a7cc04281 186533120 debug optional libcvc4-7-dbgsym_1.8-2_amd64.deb │ + b43023515d267148d17867f21f6726a2 5646040 libs optional libcvc4-7_1.8-2_amd64.deb │ + bf1e11e916f93e0b21ac919ca6f45308 131268 libdevel optional libcvc4-dev_1.8-2_amd64.deb │ + 3f464ecb7a07008404623a2e89910d26 5162116 debug optional libcvc4parser7-dbgsym_1.8-2_amd64.deb │ + 296def54c324b52003111c9fdb63d11d 365920 libs optional libcvc4parser7_1.8-2_amd64.deb ├── cvc4_1.8-2_amd64.deb │ ├── file list │ │ @@ -1,3 +1,3 @@ │ │ -rw-r--r-- 0 0 0 4 2020-09-17 16:29:09.000000 debian-binary │ │ -rw-r--r-- 0 0 0 1476 2020-09-17 16:29:09.000000 control.tar.xz │ │ --rw-r--r-- 0 0 0 79924 2020-09-17 16:29:09.000000 data.tar.xz │ │ +-rw-r--r-- 0 0 0 79976 2020-09-17 16:29:09.000000 data.tar.xz │ ├── control.tar.xz │ │ ├── control.tar │ │ │ ├── ./md5sums │ │ │ │ ├── ./md5sums │ │ │ │ │┄ Files differ │ ├── data.tar.xz │ │ ├── data.tar │ │ │ ├── ./usr/bin/cvc4 │ │ │ │┄ File has been modified after NT_GNU_BUILD_ID has been applied. │ │ │ │ ├── readelf --wide --notes {} │ │ │ │ │ @@ -1,12 +1,12 @@ │ │ │ │ │ │ │ │ │ │ Displaying notes found in: .note.ABI-tag │ │ │ │ │ Owner Data size Description │ │ │ │ │ GNU 0x00000010 NT_GNU_ABI_TAG (ABI version tag) OS: Linux, ABI: 3.2.0 │ │ │ │ │ │ │ │ │ │ Displaying notes found in: .note.gnu.build-id │ │ │ │ │ Owner Data size Description │ │ │ │ │ - GNU 0x00000014 NT_GNU_BUILD_ID (unique build ID bitstring) Build ID: ac92156935d76709bbc449fbb15e48a68f79b892 │ │ │ │ │ + GNU 0x00000014 NT_GNU_BUILD_ID (unique build ID bitstring) Build ID: c36ab2d8b2df39288f7fc9161b6a2a1bf43495ab │ │ │ │ │ │ │ │ │ │ Displaying notes found in: .note.gnu.gold-version │ │ │ │ │ Owner Data size Description │ │ │ │ │ GNU 0x00000009 NT_GNU_GOLD_VERSION (gold version) Version: gold 1.16 │ │ │ │ ├── readelf --wide --decompress --hex-dump=.gnu_debuglink {} │ │ │ │ │┄ error from `readelf --wide --decompress --hex-dump=.gnu_debuglink {}`: │ │ │ │ │┄ readelf: Error: no .dynamic section in the dynamic segment │ │ │ │ │ @@ -1,7 +1,7 @@ │ │ │ │ │ │ │ │ │ │ Hex dump of section '.gnu_debuglink': │ │ │ │ │ - 0x00000000 39323135 36393335 64373637 30396262 92156935d76709bb │ │ │ │ │ - 0x00000010 63343439 66626231 35653438 61363866 c449fbb15e48a68f │ │ │ │ │ - 0x00000020 37396238 39322e64 65627567 00000000 79b892.debug.... │ │ │ │ │ - 0x00000030 079555d1 ..U. │ │ │ │ │ + 0x00000000 36616232 64386232 64663339 32383866 6ab2d8b2df39288f │ │ │ │ │ + 0x00000010 37666339 31363162 36613261 31626634 7fc9161b6a2a1bf4 │ │ │ │ │ + 0x00000020 33343935 61622e64 65627567 00000000 3495ab.debug.... │ │ │ │ │ + 0x00000030 5eec950b ^... │ │ │ ├── ./usr/share/man/man1/cvc4.1.gz │ │ │ │ ├── cvc4.1 │ │ │ │ │ @@ -1,11 +1,11 @@ │ │ │ │ │ .\" Process this file with │ │ │ │ │ .\" groff -man -Tascii cvc4.1 │ │ │ │ │ .\" │ │ │ │ │ -.TH CVC4 1 "2020-09-17" "CVC4 release CVC4_RELEASE_STRING" "User Manuals" │ │ │ │ │ +.TH CVC4 1 "2020-09-18" "CVC4 release CVC4_RELEASE_STRING" "User Manuals" │ │ │ │ │ .SH NAME │ │ │ │ │ cvc4, pcvc4 \- an automated theorem prover │ │ │ │ │ .SH SYNOPSIS │ │ │ │ │ .B cvc4 [ │ │ │ │ │ .I options │ │ │ │ │ .B ] [ │ │ │ │ │ .I file │ │ │ ├── ./usr/share/man/man5/cvc4.5.gz │ │ │ │ ├── cvc4.5 │ │ │ │ │ @@ -1,11 +1,11 @@ │ │ │ │ │ .\" Process this file with │ │ │ │ │ .\" groff -man -Tascii cvc4.5 │ │ │ │ │ .\" │ │ │ │ │ -.TH CVC4 5 "2020-09-17" "CVC4 release CVC4_RELEASE_STRING" "Languages documentation" │ │ │ │ │ +.TH CVC4 5 "2020-09-18" "CVC4 release CVC4_RELEASE_STRING" "Languages documentation" │ │ │ │ │ .SH NAME │ │ │ │ │ cvc4 \- the native input language for CVC4 │ │ │ │ │ .SH DESCRIPTION │ │ │ │ │ .B cvc4 │ │ │ │ │ is an automated theorem prover for first-order formulas with respect │ │ │ │ │ to background theories of interest. ├── libcvc4-7_1.8-2_amd64.deb │ ├── file list │ │ @@ -1,3 +1,3 @@ │ │ -rw-r--r-- 0 0 0 4 2020-09-17 16:29:09.000000 debian-binary │ │ --rw-r--r-- 0 0 0 1240 2020-09-17 16:29:09.000000 control.tar.xz │ │ --rw-r--r-- 0 0 0 5646112 2020-09-17 16:29:09.000000 data.tar.xz │ │ +-rw-r--r-- 0 0 0 1236 2020-09-17 16:29:09.000000 control.tar.xz │ │ +-rw-r--r-- 0 0 0 5644612 2020-09-17 16:29:09.000000 data.tar.xz │ ├── control.tar.xz │ │ ├── control.tar │ │ │ ├── ./md5sums │ │ │ │ ├── ./md5sums │ │ │ │ │┄ Files differ │ ├── data.tar.xz │ │ ├── data.tar │ │ │ ├── ./usr/lib/x86_64-linux-gnu/libcvc4.so.7 │ │ │ │┄ File has been modified after NT_GNU_BUILD_ID has been applied. │ │ │ │ ├── readelf --wide --notes {} │ │ │ │ │ @@ -1,8 +1,8 @@ │ │ │ │ │ │ │ │ │ │ Displaying notes found in: .note.gnu.build-id │ │ │ │ │ Owner Data size Description │ │ │ │ │ - GNU 0x00000014 NT_GNU_BUILD_ID (unique build ID bitstring) Build ID: 1425545593fba424eccb3f17d024ba2175b9ffdc │ │ │ │ │ + GNU 0x00000014 NT_GNU_BUILD_ID (unique build ID bitstring) Build ID: 3071b15577cf8133d80239a6f8c27d1248d7e7f4 │ │ │ │ │ │ │ │ │ │ Displaying notes found in: .note.gnu.gold-version │ │ │ │ │ Owner Data size Description │ │ │ │ │ GNU 0x00000009 NT_GNU_GOLD_VERSION (gold version) Version: gold 1.16 │ │ │ │ ├── strings --all --bytes=8 {} │ │ │ │ │ @@ -44619,15 +44619,15 @@ │ │ │ │ │ sat::rnd_decisiosat::propagationsat::clauses_litsat::learnts_litsat::max_literalsat::tot_literal./src/prop/minisat/simp/SimpSolvset-user-attribudeclare-primed-vexpand-definitioget-instantiatioreset-assertionscheck-sat-assumiget-unsat-assumpblock-model-valudeclare-datatypeassertions:post-produce-assertioproduce-assignmeUnrecognized informational or option key or settsmt::SmtEngine::definitionExpansnumConstantPropscnfConversionTimnumAssertionsPrenumAssertionsPoslfscCheckProofTicheckUnsatCoreTiprocessAssertionsimplifiedToFalsresourceUnitsUsez::approx::brancz::approx::gaussianElimConstructz::approx::avera │ │ │ │ │ theory::arith::iteMinMaxApplicatteConstantApplictheory::arith::attempt::searchTittempt::queueTimttempt::conflicttheory::arith::congruence::watchedVariableIsZeroedVariableIsNotZongruence::equalongruence::propaongruence::confltheory::arith::ArithCongruenceMad::unatePropagattheory::arith::dio::conflictCallio::conflictTimeis an integer variable created by the dio solverual::UpdateConflual::findConflicual::simplexConfual::recentViolatheory::arith::pqueue::enqueuesCqueue::enqueuesDqueue::enqueuesVollectionDuplicaarOrderModeDuplitheory::arith::FC::initialProcesC::UpdateConflicC::selectUpdateFtheory::arith::utheory::arith::weakening::attempeakening::succestheory::arith::f │ │ │ │ │ phase shifted trtheory::arith::SOI::initialProceOI::UpdateConfliOI::ConfMin::numOI::ConstructionOI::Conflict::Mian extensional lemma index variable from the theabstraction function for bv theotheory::bv::algebraic::NumCallsTbraic::NumSimplibraic::NumUnknowbraic::SolveTimebraic::UseHeuristheory::bv::BitblastSolver::NumClastSolver::NumTtheory::bv::lazytheory::bv::CoreSolver::NumCallsSolver::SlicerEntheory::bv::inequality::NumCallsuality::SolveTimtheory::bv::slicer::NumRepresenter::AverageFindDer::NumEqualitietheory::bv::AvgBtheory::bv::NumSolveSubstitutiontheory::bv::solvtheory::bv::NumFtandardCheckCalltheory::bv::weightComputationTimtheory::bv::NumMeated by the theory of bitvectorEagerProofGeneraA boolean variable asserted to be true to force │ │ │ │ │ variable to represent disjoint efree infinity for virtual term sinfinity 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-modeop created durinInstStrategyEnumInstantiate::Instantiations_TotaInstantiate::Duplicate_Inst_Entalicate_Inst_ModeQuantConflictFind::Entailment_ChEPR base constancreated during sg pre-skolemizatCannot get synth function: reconstruction to syncegis_unif_num_e │ │ │ │ │ miniscope-quant-SynthEngine::cegqi_lemmas_refineSynthConjecture::filtered_soluti:candidate_rewriSygusEnumerator::enumTermsRewrit:enumTermsEvalEx │ │ │ │ │ head of unif evaqe for non-ground single invocatqe for function in non-ground sifor sygus invaritemplate inferenis a termDb frespredicate to force higher-order TheoryQuantifiercardinality bound element for setheory::sets::eetheory::shared_tSharedTermsDatabtheory::strings::cdSimplificatio:regexpUnfolding:conflictsEqEngi:conflictsEagerP:lemmasEagerPrep:lemmasRegisterTstring purify sk │ │ │ │ │ theory::datatypetheory::quantifiuf_combined_cardenumeration to meet negative car │ │ │ │ │ -or extensionalit2020-09-17 04:29this expression contains an element of unknown type (such as an abstract value); its type cannot be computed until it is substitProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais an unresolved selector type pis a shared seleError in option 1844674407370955 │ │ │ │ │ +or extensionalit2020-09-18 06:29this expression contains an element of unknown type (such as an abstract value); its type cannot be computed until it is substitProofCheckerStatistics::ruleChecistics::totalRulPRefProofGeneratTConvProofGenerais an unresolved selector type pis a shared seleError in option 1844674407370955 │ │ │ │ │ resource::Bitblaresource::BvEageresource::BvPropresource::BvSatCresource::CnfSteresource::Decisiresource::LemmaSresource::ParseSresource::Preproresource::Quantiresource::Restarresource::Rewritresource::SatConresource::Theory │ │ │ │ │ is a skolem variable imported from another ExprM │ │ │ │ │ approx-branch-dearith-no-partialarith-prop-clausarith-rewrite-eqcollect-pivot-sterror-selection-heuristic-pivotsmaxCutsInContextnl-ext-tf-taylorpp-assert-max-suprop-row-length=replay-early-cloreplay-failure-preplay-num-err-preplay-reject-cureplay-soi-major-threshold-pen=Nreplay-soi-minorsimplex-check-pestandard-effort-variable-order-parrays-eager-indarrays-lazy-rintarrays-optimize-arrays-reduce-sharrays-weak-equistats-every-querstats-hide-zerosbv-algebraic-budbv-eager-explanabv-eq-slicer=MODbv-extract-arithbv-inequality-sobv-lazy-reduce-ebv-lazy-rewrite-bv-optimize-sat-bv-print-consts-as-indexed-symbobv-proof-format=dt-infer-as-lemmdt-rewrite-errorsygus-sym-break-decision-random-decision-threshodecision-use-weidecision-weight-print-expr-typesinteractive-promtear-down-incremfilesystem-accesglobal-declaratiflatten-ho-chaininst-format=MODEmodel-format=MODaggressive-core-allow-empty-depefewer-preprocesslfsc-letificatiominisat-dump-dimminisat-eliminatrandom-frequencyrefine-conflictsrestart-int-baserestart-int-inc=ag-miniscope-quacegis-sample=MODcegqi-bv-concat-cegqi-bv-ineq=MOcegqi-bv-interlecegqi-bv-rm-extrcegqi-bv-solve-ncegqi-multi-instcegqi-prereg-inscegqi-repeat-litcegqi-round-up-lcegqi-use-inf-incegqi-use-inf-recond-var-split-acond-var-split-qconjecture-filteconjecture-gen-gconjecture-gen-mconjecture-gen-pconjecture-gen-uconjecture-no-fidt-var-exp-quantelim-ext-arith-qext-rewrite-quanfinite-model-finfull-saturate-quho-elim-store-axho-matching-var-ho-merge-term-dbincrement-triggeinst-max-level=Ninst-no-model-trinst-when-phase=inst-when-strictinst-when-tc-firite-dtt-split-quite-lift-quant=Mliteral-matchinglte-restrict-insmacros-quant-modmbqi-one-inst-pemulti-trigger-camulti-trigger-prpartial-triggerspre-skolem-quantprenex-quant-useprenex-quant=MODpure-th-triggerspurify-dt-triggeqcf-all-conflictqcf-eager-check-qcf-nested-conflquant-anti-skolequant-cf-when=MOquant-dsplit-modquant-rep-mode=Mregister-quant-brelational-triggsygus-active-gensygus-add-const-sygus-arg-relevasygus-auto-unfolsygus-bool-ite-rsygus-core-connesygus-crepair-absygus-eval-unfolsygus-expr-miner-check-use-exporsygus-grammar-cosygus-grammar-nosygus-inv-templ-sygus-inv-templ=sygus-pbe-multi-sygus-qe-preprocsygus-query-gen-sygus-rec-fun-evsygus-repair-consygus-rr-synth-asygus-rr-synth-csygus-rr-synth-fsygus-rr-synth-rsygus-rr-verify-sygus-sample-fp-sygus-sample-grasygus-si-partialsygus-si-rcons-lsygus-si-rcons=Msygus-si-reconstsygus-templ-embesygus-unif-cond-independent-no-rsygus-unif-pi=MOsygus-unif-shuffsygus-verify-subterm-db-mode=MODtrack-inst-lemmatrigger-active-strigger-sel=MODEvar-ineq-elim-qusep-pre-skolem-esets-infer-as-lesets-proxy-lemmablock-models=MODbv-eager-assert-check-unsat-coredebug-check-modediagnostic-outpudump-instantiatidump-unsat-coresext-rew-prep-aggforce-no-limit-cinteractive-modemodel-cores=MODEmodel-witness-vaon-repeat-ite-siproduce-unsat-asproduce-unsat-coreproducible-ressat-conflict-stesimplification-msygus-print-calltheory-check-stere-inter-mode=MOstrings-guess-mostrings-infer-asstrings-infer-systrings-len-normstrings-min-prefstrings-print-asstrings-process-strings-rexplainassign-function-uf-symmetry-breauf-ss-abort-carduf-ss-totality-luf-ss-totality-sN4CVC47context10ContextObjE │ │ │ │ │ N4CVC47context16ContextNotifyObjE │ │ │ │ │ N4CVC47context6CDListINS_12NodeTemplateILb1EEENS0_14DefaultCleanUpIS3_EESaIS3_EEE │ │ │ │ │ N4CVC47context3CDOINS_4prop8SatValueEEE │ │ │ │ │ N4CVC48decision16DecisionStrategyE │ │ │ │ ├── .text │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .fini │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .rodata │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .gcc_except_table │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .eh_frame │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .eh_frame_hdr │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .tbss │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .data.rel.ro.local │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .fini_array │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .init_array │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .data.rel.ro │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .got │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .got.plt │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .data │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .tm_clone_table │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .bss │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .gnu_debuglink │ │ │ │ │┄ Timeout exceeded; details may be incomplete. │ │ │ │ ├── .shstrtab │ │ │ │ │┄ Timeout exceeded; details may be incomplete. ├── libcvc4-dev_1.8-2_amd64.deb │┄ Timeout exceeded; details may be incomplete. ├── libcvc4parser7_1.8-2_amd64.deb │┄ Timeout exceeded; details may be incomplete. ├── cvc4-dbgsym_1.8-2_amd64.deb │┄ Timeout exceeded; details may be incomplete. ├── libcvc4-7-dbgsym_1.8-2_amd64.deb │┄ Timeout exceeded; details may be incomplete. ├── libcvc4parser7-dbgsym_1.8-2_amd64.deb │┄ Timeout exceeded; details may be incomplete.