summaryrefslogtreecommitdiff
BranchCommit messageAuthorAge
1.0.xfix up build system for swig (d242c30 introduced a subtle error)Morgan Deters11 years
1.1.xbug 374 fix: assert litVal=desiredVal only for leaf nodesKshitij Bansal11 years
1.2.xbug 374 fix: assert litVal=desiredVal only for leaf nodesKshitij Bansal11 years
1.3.xFixing bug 552. There was a bug when integers are made using a string with a...Tim King10 years
1.4.xremove options infrastructure code which depended on undefined behaviorKshitij Bansal8 years
CIAddFlex[CI] Update package listAndres Noetzli4 years
abstractValsUnify abstract values and uninterpreted constantsAndres Noetzli3 years
abstractValsPRUnify abstract values and uninterpreted constantsAndres Noetzli3 years
actions-ci-prMake a unit test failAndres Noetzli4 years
addLemmasreplace lemmaAndres Noetzli5 years
addVerifyTestsMerge branch 'master' into addVerifyTestsAndrew Reynolds6 years
aggCDSimpAggressive CD simplificationsAndres Noetzli4 years
aggSkolemSharingMerge branch 'revertMoveSSCombine' into aggSkolemSharingAndres Noetzli5 years
aggSkolemSharingAltminorAndres Noetzli5 years
alwaysDeleteProofFilesDelete temporary proof files when aborting CVC4Andres Noetzli5 years
an/refactor/NodeBuilderRemove template argument from `NodeBuilder`Andres Noetzli3 years
anonStrPRremove experimentsAndres Noetzli5 years
anonymizeStringsremove experimentsAndres Noetzli5 years
archiveRunScriptsMerge branch 'master' into archiveRunScriptsMathias Preiner3 years
arr_rewriter_refactorMove array rewriter functions to source fileAndres Notzli8 years
arrayConstFaster isConstAndres Noetzli3 years
assignment3Fix edge directionAndres Noetzli4 years
betterSkolems2minorAndres Noetzli5 years
betterStripSymbolicLengthupdateAndres Noetzli5 years
bidirQuantInstBidirectional quantifier instantiationAndres Noetzli5 years
bogusAssertionsFix bogus assertionsAndres Noetzli5 years
bool-terms-with-skolemstodoDejan Jovanovic9 years
boolean-term-reorganother test caseDejan Jovanovic9 years
braced-init-listMerge branch 'master' into braced-init-listAndres Noetzli3 years
cacheReplSkolemsCache replace skolemsAndres Noetzli6 years
cav2019stringsAdd counterAndres Noetzli5 years
cav2019strings_countRewRedmergeAndres Noetzli5 years
cav2019strings_expnew rewriteAndres Noetzli5 years
cav2020Length requirements in conclusionsAndres Noetzli4 years
cav2020submissionStats per skolem idAndres Noetzli4 years
cav22-stringsMerge branch 'master' into cav22-stringsAndrew Reynolds2 years
changeAssocChange FlattenAssocCommut rewriteAndres Noetzli5 years
changeRegStrings: Register skolems before sending lemmaAndres Noetzli4 years
check_exceptionsAdd check for C++ exceptions to config scriptAndres Notzli7 years
clang-tidytest2Andres Noetzli4 years
clean_includesmore cleanupAndres Noetzli7 years
cleanup_outputMerge branch 'master' into cleanup_outputMathias Preiner6 years
codeStringsupport for code.strAndres Noetzli5 years
compiler_infofixAndres Noetzli6 years
countRewRedfixAndres Noetzli5 years
coverity1473023Merge branch 'master' into coverity1473023Andres Noetzli6 years
createCheckEntailContainsMerge branch 'master' into createCheckEntailContainsAndrew Reynolds5 years
cxxtest_pkgAdd cxxtest as packageAndres Notzli7 years
d_slow_regMerge branch 'master' into d_slow_regAndres Noetzli6 years
dedup_langFormattingAndres Noetzli6 years
deleteInvalidMkConstMerge branch 'master' into deleteInvalidMkConstAndrew Reynolds2 years
develRe-enabling properConflict assertionClark Barrett9 years
differentIndexHeuristicDifferent heuristicAndres Noetzli4 years
disableAggRegexdisable agg regexAndres Noetzli4 years
divModSemMerge branch 'master' into divModSemAina Niemetz4 years
div_semanticsMerge branch 'master' into div_semanticsAndrew Reynolds7 years
docMerge branch 'master' into docAina Niemetz4 years
docsLinkMerge branch 'master' into docsLinkAndres Noetzli3 years
dslverificationAndres Noetzli3 years
duplicate_lemmasbackjumping to make propagation lemmas currentDejan Jovanovic8 years
eatmydataquick testAndres Noetzli6 years
emptyEqMerge branch 'master' into emptyEqAndrew Reynolds6 years
emptyStrRewritesfixAndres Noetzli6 years
eqNotifyRewritelazy registrationAndres Noetzli4 years
esolverPrototypeProtype e-solver implementationAndres Noetzli3 years
evalFallbackAndres Noetzli6 years
eval3Evaluator: support other theories for equalityAndres Noetzli6 years
eval4Fix hanging evaluatorAndres Noetzli6 years
eval5Fix CONST_RATIONAL conversion in evaluationAndres Noetzli6 years
eval6Evaluator: support and/or, contains, prefix/suffixAndres Noetzli6 years
evalStrCodeMerge branch 'master' into evalStrCodeAndrew Reynolds6 years
eval_fpAdd floating-point support in evaluatorAndres Noetzli6 years
experimentPartial fix for bug 717.Clark Barrett7 years
experimentalFixing cryptominisat build issuesLiana Hadarean8 years
exprManagerConstrPrivateMerge branch 'master' into exprManagerConstrPrivateAndres Noetzli4 years
ext_decMerge remote-tracking branch 'ajreynol/extDecomposeRevisit' into ext_decAndres Noetzli5 years
extfSubstMore aggressive substitutions for extf evalAndres Noetzli4 years
fasterCompilationImprove compile timesAndres Noetzli6 years
finalOptsMerge branch 'master' into finalOptsAndres Noetzli3 years
fix-cln-static-downloadMerge branch 'master' into fix-cln-static-downloadAndrew Reynolds2 years
fix1649Merge branch 'master' into fix1649Gereon Kremer3 years
fix2002Merge branch 'master' into fix2002Andres Noetzli6 years
fix2982Merge branch 'master' into fix2982Andrew Reynolds5 years
fix3020Avoid substituting Boolean term variablesAndres Noetzli5 years
fix3089Merge branch 'master' into fix3089Andrew Reynolds5 years
fix3475Merge branch 'master' into fix3475Andrew Reynolds5 years
fix3683Fix arithmetic rewriter for exponentialAndres Noetzli4 years
fix3959Merge branch 'master' into fix3959Andrew Reynolds4 years
fix3991Merge branch 'master' into fix3991Andrew Reynolds4 years
fix4376Reinstantiate support for conjunctions in factsAndres Noetzli4 years
fix4477Merge branch 'master' into fix4477Andrew Reynolds4 years
fix4644[unconstrained] Fix gathering of visited-once varsAndres Noetzli4 years
fix4658Fix memory leak in unit test node_algorithm_blackAndres Noetzli4 years
fix4771Fix 4771Andres Noetzli4 years
fix5024Merge branch 'master' into fix5024Andrew Reynolds4 years
fix5090Merge branch 'master' into fix5090Andrew Reynolds4 years
fix6520Merge branch 'master' into fix6520Mathias Preiner3 years
fix6639Merge branch 'master' into fix6639Andrew Reynolds3 years
fix7017minorAndres Noetzli3 years
fixABCMerge branch 'master' into fixABCAndrew Reynolds4 years
fixANTLRFix `ANTLR3_COMMAND` for system ANTLR3 JARAndres Noetzli3 years
fixANTLRBuildMerge branch 'master' into fixANTLRBuildAndres Noetzli3 years
fixAmazonFix linking ANTLR3 on some systemsAndres Noetzli3 years
fixArithLemmasFix arith lemmas for mod/divAndres Noetzli4 years
fixArithLemmasPRFix Arith lemmas for div/modAndres Noetzli4 years
fixAsanfixAndres Noetzli6 years
fixAsanInteractiveShellBlackMerge branch 'master' into fixAsanInteractiveShellBlackAndrew Reynolds4 years
fixBetterSkolemsMerge branch 'master' into fixBetterSkolemsAndres Noetzli5 years
fixBiasMerge branch 'master' into fixBiasAlex Ozdemir5 years
fixCI[CI] Fix Cython installationAndres Noetzli4 years
fixCMSBuildFix CryptoMiniSat build, regressionAndres Noetzli4 years
fixCMSBuildPRMerge branch 'master' into fixCMSBuildPRAndrew Reynolds4 years
fixClangWarningsMerge branch 'master' into fixClangWarningsAndres Noetzli3 years
fixCollectEmptyEqsMerge branch 'master' into fixCollectEmptyEqsAndres Noetzli6 years
fixConfigureTypoMerge branch 'master' into fixConfigureTypoAina Niemetz6 years
fixDestrOrderMerge branch 'master' into fixDestrOrderAlex Ozdemir5 years
fixDumpMerge branch 'master' into fixDumpAndres Noetzli6 years
fixEagerModelsMerge branch 'master' into fixEagerModelsAina Niemetz5 years
fixErrorSetMerge branch 'master' into fixErrorSetAndrew Reynolds3 years
fixEvalIdOfMerge branch 'master' into fixEvalIdOfAndrew Reynolds6 years
fixExamplesFix use of APPLY kind in examplesAndres Noetzli5 years
fixExportToMerge branch 'master' into fixExportToAndrew Reynolds6 years
fixExtraVersionMerge branch 'master' into fixExtraVersionAndrew Reynolds4 years
fixFPboolFix fp-bool.sy grammar and require symfpuAndres Noetzli6 years
fixGetUnsatAssumptDumpMerge branch 'master' into fixGetUnsatAssumptDumpAina Niemetz6 years
fixGlpkBuildFix GLPK build on older CMake versionsAndres Noetzli3 years
fixInConflictRevert semantic change from refactoringAndres Noetzli4 years
fixIssue3596Merge branch 'master' into fixIssue3596Andrew Reynolds4 years
fixIssue5074Merge branch 'master' into fixIssue5074Andrew Reynolds4 years
fixJavaConfigMerge branch 'master' into fixJavaConfigAndres Noetzli3 years
fixJavaTestsMerge branch 'master' into fixJavaTestsAina Niemetz4 years
fixLib64updateAndres Noetzli3 years
fixLineNrWarnsMerge branch 'master' into fixLineNrWarnsAndrew Reynolds5 years
fixLinkingMerge branch 'master' into fixLinkingAndres Noetzli3 years
fixMacBuildMerge branch 'master' into fixMacBuildAndres Noetzli6 years
fixMacOsActionFix GitHub Actions macOS buildAndres Noetzli3 years
fixMemLeakFix memory leak in unit testAndres Noetzli5 years
fixNightliesUse uniform length limit for String constantsAndres Noetzli6 years
fixNightliesNoProof[Regressions] Require proof support for abductionAndres Noetzli4 years
fixNightlyAsanC++ API: Fix OOB read in unit testAndres Noetzli5 years
fixNightlyCompMerge branch 'master' into fixNightlyCompAndrew Reynolds4 years
fixNodeTraversalMerge branch 'master' into fixNodeTraversalAndrew Reynolds4 years
fixNonDumpingMerge branch 'master' into fixNonDumpingAndres Noetzli6 years
fixOptionsDepMerge branch 'master' into fixOptionsDepAndrew Reynolds3 years
fixPPDumpPRFix dumping pre/post preprocessing passesAndres Noetzli6 years
fixPPregMerge branch 'master' into fixPPregAndrew Reynolds6 years
fixPR2737fixAndres Noetzli5 years
fixParseOnlyMerge branch 'master' into fixParseOnlyAndrew Reynolds3 years
fixPayloadSeenFix redundant definitions of `NodeValue::getConst`Andres Noetzli3 years
fixPolyMerge branch 'master' into fixPolyAndres Noetzli6 years
fixPrinterAdd support for printing `re.loop` and `re.^`Andres Noetzli4 years
fixRefCountZeroMerge branch 'master' into fixRefCountZeroAndrew Reynolds4 years
fixRegMerge branch 'master' into fixRegAndres Noetzli5 years
fixRegNightliesMerge branch 'master' into fixRegNightliesAndrew Reynolds5 years
fixRegression4971Make regression test `issue4971-0` more robustAndres Noetzli3 years
fixRevInferenceFix reverse inferenceAndres Noetzli4 years
fixSetInfoNameMerge branch 'master' into fixSetInfoNameAndrew Reynolds6 years
fixSolverBlackAmbiguityMerge branch 'master' into fixSolverBlackAmbiguityAina Niemetz4 years
fixStaticInstallMerge branch 'master' into fixStaticInstallAndrew Reynolds4 years
fixStrLitParserMerge branch 'master' into fixStrLitParserAndrew Reynolds5 years
fixStrRegressMerge branch 'master' into fixStrRegressAndrew Reynolds3 years
fixStrictParsingMerge branch 'master' into fixStrictParsingAina Niemetz6 years
fixStrictParsingBvOpMerge branch 'master' into fixStrictParsingBvOpAndres Noetzli5 years
fixTearDownIncrementalFix --tear-down-incrementalAndres Noetzli3 years
fixWShadowMerge branch 'master' into fixWShadowAndres Noetzli4 years
fixWinBuildMerge branch 'master' into fixWinBuildAndres Noetzli3 years
fixWinTypesMerge branch 'master' into fixWinTypesAndrew Reynolds4 years
fix_cdlistMerge branch 'master' into fix_cdlistAndres Noetzli3 years
fix_cmm_unit_testMerge branch 'master' into fix_cmm_unit_testAndres Noetzli6 years
fix_dist_build2Fix typo in Makefile that makes distcheck failAndres Notzli8 years
fix_eqproof[LFSC] Fix memory leaksAndres Noetzli7 years
fix_java_testsfix java testsAndres Noetzli7 years
fix_lfsc_mem_leaks[LFSC] Fix memory leaks when creating CExprsAndres Notzli7 years
fix_mem_leaksAvoid mixing new/delete with malloc/freeAndres Notzli7 years
fix_proof_spacesFix missing/redundant spaces in proofsAndres Notzli8 years
fix_rewriteFix minor bug and typo in boolean rewriterAndres Notzli8 years
fix_runscriptFix no-cbqi-innermost option name in run scriptAndres Noetzli6 years
fix_sat_solverFixAndres Noetzli6 years
fix_shared_winFix shared libraries for Windows buildAndres Notzli7 years
fix_typosFix some typos, fix some formatting, minor cleanupAndres Notzli8 years
fix_unsat_coresupdate run regression scriptAndres Noetzli7 years
fix_warnsMerge branch 'master' into fix_warnsAndres Noetzli6 years
fix_win_gmpMerge branch 'master' into fix_win_gmpAndres Noetzli6 years
fmcad2020-stringsAdd skolem stats and sharing toggleAndres Noetzli4 years
fp_to_ieee_bvAdd support for fp.to_ieee_bvAndres Noetzli4 years
from_master_fix_compile_speedfixAndres Noetzli7 years
from_master_fix_lfsc_leaks[LFSC] Fix memory leaks related to IntExpr/RatExprAndres Noetzli7 years
ghActionsTestAndres Noetzli4 years
googleMinor fixes for inst match generators. Updates to qip.ajreynol8 years
hackblaAndres Noetzli4 years
ijcar2020Option for toggling str.codeAndres Noetzli4 years
ijcar2020_crOption for toggling str.codeAndres Noetzli4 years
inc-adj-listRevert "Slightly better sorting key"Matthew Sotoudeh2 years
includesMerge branch 'master' into includesAndrew Reynolds3 years
incremental-adj-for-dirtyThis seems to be the best of the past few commitsMatthew Sotoudeh2 years
incremental-adjacent-try3More like best than inc-adjMatthew Sotoudeh2 years
incremental-current-bestThis seems to be the best of the past few commitsMatthew Sotoudeh2 years
incremental-no-hashmapRemove the rest of my CDHashMapsMatthew Sotoudeh2 years
indexof_reMerge branch 'master' into indexof_reAndrew Reynolds3 years
ineq_assumptionsMerge branch 'master' into ineq_assumptionsAndrew Reynolds6 years
inferZerofix mergeAndres Noetzli6 years
input-parserAdd new interface for parsing inputsAndres Noetzli3 years
issue4028Merge branch 'master' into issue4028Aina Niemetz4 years
issue4070Merge branch 'master' into issue4070Andres Noetzli4 years
issue4077Merge branch 'master' into issue4077Aina Niemetz4 years
issue4151Merge branch 'master' into issue4151Aina Niemetz4 years
issue4367Merge branch 'master' into issue4367Andrew Reynolds4 years
issue4576Merge branch 'master' into issue4576Andrew Reynolds4 years
issue5330Merge branch 'master' into issue5330Andrew Reynolds4 years
issue6453Merge branch 'master' into issue6453Andrew Reynolds3 years
issue6636Merge branch 'master' into issue6636Andres Noetzli3 years
issue6643Merge branch 'master' into issue6643Mathias Preiner3 years
issue6661Merge branch 'master' into issue6661Andrew Reynolds3 years
issue6717Merge branch 'master' into issue6717Haniel Barbosa3 years
issue6834Merge branch 'master' into issue6834Andrew Reynolds3 years
issue7056Merge branch 'master' into issue7056Andres Noetzli3 years
issue7504Merge branch 'master' into issue7504Gereon Kremer3 years
issue7569Merge branch 'master' into issue7569Mathias Preiner3 years
kindSkolemsmore rewritesAndres Noetzli4 years
lenInConcMove length requirements to conclusionAndres Noetzli4 years
lengthPreserveAddress commentAndres Noetzli6 years
leqRewMerge branch 'master' into leqRewAndrew Reynolds3 years
lessRewritesless rewritesAndres Noetzli5 years
lfscTestsMerge branch 'master' into lfscTestsAndrew Reynolds4 years
libdirANTLR3: Install into `CMAKE_INSTALL_LIBDIR`Andres Noetzli3 years
link_smt:link-smtAndres Noetzli6 years
m1buildMerge branch 'master' into m1buildAndres Noetzli3 years
macos11Merge branch 'master' into macos11Andres Noetzli3 years
mapConstRationalminorAndres Noetzli3 years
masterFix `collectEmptyEqs()` in string utilsAndres Noetzli3 years
matthew-bellman-non-incUpdate rewriterMatthew Sotoudeh2 years
mergePostSuffixminAndres Noetzli5 years
mergePostSuffix2nitAndres Noetzli5 years
miscWarnsMerge branch 'master' into miscWarnsAndrew Reynolds6 years
mkExceptionPublicMerge branch 'master' into mkExceptionPublicAndres Noetzli3 years
moveDetectLoopMove detect loopAndres Noetzli5 years
moveKindedMerge branch 'master' into moveKindedAndrew Reynolds6 years
moveSlowRegMove slow string regression to regress3Andres Noetzli5 years
move_constrimplement move constructor for nodesAndres Noetzli7 years
move_visitorMerge branch 'master' into move_visitorAndrew Reynolds6 years
mpfrMPFR supportAndres Noetzli6 years
mult_argsMerge branch 'master' into mult_argsAina Niemetz6 years
multiple-cycles-quickFix bugs in reporting multiple cyclesMatthew Sotoudeh2 years
newApiForCommandsSketch of refactoring the Commands to use new APIAndres Noetzli6 years
newCtnInfupdateAndres Noetzli5 years
newCtnRMerge branch 'master' into newCtnRAndrew Reynolds6 years
newSubstrNew reduction for str.substrAndres Noetzli3 years
newlMerge branch 'master' into newlAndrew Reynolds6 years
next_model_cherry_fixFix interface for bindingsAndres Noetzli5 years
noNormalLoopBreakno normal loop breakingAndres Noetzli5 years
nodeArrayStoreAllMerge branch 'master' into nodeArrayStoreAllAndrew Reynolds4 years
nodeAssertionListminorAndres Noetzli4 years
nodeEmptySetTowards Node-level SmtEngineAndres Noetzli4 years
nodeEmptySetPRMerge branch 'master' into nodeEmptySetPRAndres Noetzli4 years
nodeUConstMerge branch 'master' into nodeUConstAndrew Reynolds4 years
nodeViewformatAndres Noetzli3 years
normalFormsHeuristicNew normal forms heuristicAndres Noetzli5 years
normalFormsHeuristic2Take into account exp sizeAndres Noetzli5 years
normalizeStringsSkolemAggminorAndres Noetzli5 years
notCtnRedalt versionAndres Noetzli5 years
nprocMerge branch 'master' into nprocAndres Noetzli3 years
oldVarHeuristicPrefer old variable heuristicAndres Noetzli4 years
oldVarHeuristicPRMerge branch 'master' into oldVarHeuristicPRAndrew Reynolds4 years
oneWeirdRewriteone weird rewriteAndres Noetzli5 years
optExpoptimize explanationsAndres Noetzli4 years
optNormalFormMinor optimizationAndres Noetzli4 years
optStringHashFaster hasing for `cvc5::String`Andres Noetzli2 years
optimizeRunscriptSLIAMerge branch 'master' into optimizeRunscriptSLIAAndrew Reynolds5 years
overlapexperimentAndres Noetzli5 years
parser-stateSplit parser state from parser classAndres Noetzli3 years
paserNamedErrorMsgMerge branch 'master' into paserNamedErrorMsgAndrew Reynolds3 years
pldi2019Move ss-combine rewrite to extended rewriterAndres Noetzli6 years
postreleaseMerge branch 'master' into postreleaseAndres Noetzli4 years
prePostKindsMerge branch 'revertMoveSSCombine' into prePostKindsAndres Noetzli5 years
prefixesaggressive prefix deductionAndres Noetzli4 years
pri_user_langMerge branch 'master' into pri_user_langAndres Noetzli6 years
printHistogramKindsMerge branch 'master' into printHistogramKindsAndrew Reynolds4 years
privateGetMerge branch 'master' into privateGetAndrew Reynolds3 years
projIssue316Merge branch 'master' into projIssue316Andrew Reynolds3 years
projIssue327[FP] Fix overly restrictive assertionAndres Noetzli3 years
projIssue340Merge branch 'master' into projIssue340Andrew Reynolds3 years
proof-new-dsltmpAndres Noetzli3 years
python3.5regMerge branch 'master' into python3.5regAndrew Reynolds3 years
quantifier_proofsSupport for quantifier proofsAndres Noetzli6 years
quantifier_proofs_Support for quantifier proofsAndres Noetzli5 years
quickLenConflictDetect conflict quicklyAndres Noetzli4 years
reAllSupportMerge branch 'master' into reAllSupportAndrew Reynolds5 years
reAllSupport2minorAndres Noetzli5 years
reElimChangeChange re-elimAndres Noetzli4 years
reInterRewRewrites for re.interAndres Noetzli5 years
reLoopRewRewrite for re.loopAndres Noetzli5 years
recordAssumptionsRecord assumption info in AssertionPipelineAndres Noetzli6 years
reduceReplacePRfixAndres Noetzli6 years
reenableContextBlackMerge branch 'master' into reenableContextBlackAndres Noetzli3 years
reenableSSCombineReenable ss-combineAndres Noetzli5 years
refactorArrayCoreSolverMerge branch 'master' into refactorArrayCoreSolverAndrew Reynolds2 years
refactorEagerSolverMerge branch 'master' into refactorEagerSolverAndrew Reynolds3 years
refactorProcessSimpleDeqRefactor CoreSolver::processSimpleDeqAndres Noetzli4 years
refactorProcessSimpleDeqPRMerge branch 'master' into refactorProcessSimpleDeqPRAndrew Reynolds4 years
refactorTheoryBoolRewriterRefactor TheoryBoolRewriter to use rewriter tablesAndres Noetzli4 years
refactorUnconstrainedSimpMerge branch 'master' into refactorUnconstrainedSimpAndres Noetzli6 years
refactor_ppXExample for refactoringAndres Notzli7 years
refactor_pp_backupfixed timer issueJustin Xu7 years
refactor_pp_registryInitial work on PreprocessingPassRegistryAndres Noetzli7 years
regDisableProofsMerge branch 'master' into regDisableProofsAndrew Reynolds4 years
regWDefaultCmdLineMerge branch 'master' into regWDefaultCmdLineAndrew Reynolds5 years
regexRRVerifyMerge branch 'master' into regexRRVerifyAndrew Reynolds6 years
regexpBidirUnfoldUnfold regexps two waysAndres Noetzli4 years
remove-cd-dense-setAlso remove cddense_set.h from the CMakeListMatthew Sotoudeh2 years
removeBinaryCspRemove `--strings-binary-csp` optionAndres Noetzli4 years
removeBinaryCspPRRemove `--strings-binary-csp` optionAndres Noetzli4 years
remove_in_assertionsRemove input assertionsAndres Notzli7 years
remove_throw[Coverity] Remove throw qualifiers in src/smtAndres Notzli7 years
renameJavaPackageMerge branch 'master' into renameJavaPackageAndrew Reynolds4 years
replSubstaddress commentAndres Noetzli6 years
replaceReplacefix commentAndres Noetzli6 years
replaceRewritesMerge branch 'master' into replaceRewritesAndrew Reynolds6 years
replaceRewritesCacheskolem fnsAndres Noetzli6 years
replaceSubstituteMerge branch 'sygusComp2018-2' into replaceSubstituteAndres Noetzli6 years
replace_reAdd support for str.replace_re(_all)Andres Noetzli4 years
replreplRewMerge branch 'master' into replreplRewAndrew Reynolds6 years
revIterMerge branch 'master' into revIterAndres Noetzli3 years
reverseSkolemMapcontdAndres Noetzli4 years
revertMoveSSCombineRevert "Move ss-combine rewrite to extended rewriter (#2703)"Andres Noetzli5 years
rewContainstest rewriteAndres Noetzli4 years
rewContainsPRMerge branch 'master' into rewContainsPRAndrew Reynolds4 years
rewIndexOfStrengthen str.indexof rewriteAndres Noetzli6 years
rewInferless aggressiveAndres Noetzli5 years
rewriteREtoContainsAdd rewrite for contains + const strings replaceAndres Noetzli5 years
rewrite_concatMerge branch 'master' into rewrite_concatAndrew Reynolds6 years
rewrite_proofSupport rewrite proofs in the theory of arraysAndres Notzli8 years
rewrite_proof_testminor changesAndres Noetzli7 years
rm-bv-div-zero-const-refsMerge branch 'master' into rm-bv-div-zero-const-refsAndrew Reynolds3 years
rmAliasesMerge branch 'master' into rmAliasesAndrew Reynolds4 years
rmBindingsParserfixAndres Noetzli4 years
rmCDAttrMerge branch 'master' into rmCDAttrAndres Noetzli3 years
rmCoverityMerge branch 'master' into rmCoverityAina Niemetz6 years
rmExprSequenceMerge branch 'master' into rmExprSequenceAndrew Reynolds4 years
rmHeuristicMerge branch 'master' into rmHeuristicAndrew Reynolds4 years
rmMaybeMerge branch 'master' into rmMaybeAndrew Reynolds3 years
rmNoInteractivePromptMerge branch 'master' into rmNoInteractivePromptAndrew Reynolds3 years
rmOutdatedMerge branch 'master' into rmOutdatedAina Niemetz6 years
rmPostsolveRemove unused postsolve infrastructureAndres Noetzli4 years
rmStateOptionsMerge branch 'master' into rmStateOptionsAndrew Reynolds3 years
rmStaticRemove staticAndres Noetzli5 years
rmTearDownIncrementalMerge branch 'master' into rmTearDownIncrementalAndres Noetzli3 years
rmUnusedNmFnsMerge branch 'master' into rmUnusedNmFnsAndrew Reynolds3 years
rm_cd_set_collectionMerge branch 'master' into rm_cd_set_collectionAndres Noetzli6 years
rm_cdchunklist2Address Andy's commentAndres Noetzli6 years
rm_cdvectorMerge branch 'master' into rm_cdvectorAina Niemetz6 years
rm_invalid_regMerge branch 'master' into rm_invalid_regAndrew Reynolds6 years
rm_svnMerge branch 'master' into rm_svnAndrew Reynolds6 years
rm_tlsMerge branch 'master' into rm_tlsAndres Noetzli6 years
run_new_logicsMerge branch 'master' into run_new_logicsAndrew Reynolds6 years
safePrintInferencesMerge branch 'master' into safePrintInferencesAndrew Reynolds4 years
sat2019Move ss-combine rewrite to extended rewriterAndres Noetzli6 years
sendExplLemmaSend explanation lemmaAndres Noetzli4 years
skipRegMerge branch 'master' into skipRegAndrew Reynolds4 years
smtcomp2019_fixedAvoid printing "success" for forced logicAndres Noetzli5 years
smtcomp2020starexec[SMT-COMP] Redirect non-answers to /dev/nullAndres Noetzli4 years
smtcomp2021Final update to SMT-COMP 2021 optionsAndres Noetzli3 years
smtcomp2021-fixedAdd branch and bound lemma if linear arithmetic generates a non-integer assig...Andrew Reynolds3 years
smtcompoptsMerge branch 'master' into smtcompoptsAndrew Reynolds3 years
solveEqRew.Andres Noetzli5 years
splitEqLensplit len constsAndres Noetzli4 years
splitEqRewMerge branch 'master' into splitEqRewAndrew Reynolds5 years
starter-bellman-incRemove the rest of my CDHashMapsMatthew Sotoudeh2 years
starter-inc-longsDirty nodes for the int64_t oneMatthew Sotoudeh2 years
starterProjectFix the rewriterMatthew Sotoudeh2 years
stdAttrsMerge branch 'master' into stdAttrsMathias Preiner3 years
strRewritesMerge branch 'master' into strRewritesAndrew Reynolds6 years
stratRe-062019_expfixAndres Noetzli5 years
stringReplaceUsingIndexOfUse str.indexof in str.replace reductionAndres Noetzli3 years
stringsPfFixCycleDetectFix detection of cyclic proofsAndres Noetzli4 years
stringsPfRewriterPRMinorAndres Noetzli4 years
stringsSkolemLenFixProtect length requirementsAndres Noetzli4 years
strongerContainsRewMinorAndres Noetzli5 years
subsolverParamsMerge branch 'master' into subsolverParamsAndres Noetzli6 years
substrsubstrAdd length-based rewrites for (str.substr _ _ _)Andres Noetzli6 years
summary_foldersRestrict test summary to first-level subfoldersAndres Noetzli6 years
sygus2018stringsRewMerge branch 'master' into sygus2018stringsRewAndrew Reynolds6 years
testtest codeAndres Noetzli7 years
theoryElimContextMerge branch 'master' into theoryElimContextAndres Noetzli3 years
theoryRewritersAddressAndres Noetzli4 years
travis_timingTravis timingAndres Noetzli6 years
udiv_constminor fixAndres Noetzli6 years
ufSkolemsfixAndres Noetzli4 years
unordered_maps_pull_request_fixalso fix for tptpAndres Noetzli7 years
unsat_assum_regMerge branch 'master' into unsat_assum_regAina Niemetz6 years
unsat_core_exampleexampleAndres Notzli8 years
up-fix-fixUse TMPDIR environment variable for temp filesAndres Noetzli5 years
update1.9newsMerge branch 'master' into update1.9newsAndrew Reynolds4 years
updateCvc5h[API] Update comments w.r.t. SymFPUAndres Noetzli3 years
updateLangHelpUpdate `--lang=help`Andres Noetzli3 years
updateRunScripts[SMT-COMP 2019] Update run scripts to match tracksAndres Noetzli5 years
updateScriptsMerge branch 'master' into updateScriptsAndres Noetzli4 years
warn_spacesMerge branch 'master' into warn_spacesAndrew Reynolds6 years
weakenCheckUnsatCoreMerge branch 'master' into weakenCheckUnsatCoreAndrew Reynolds4 years
win_deps_tmpremove exitAndres Noetzli7 years
wshadowformatAndres Noetzli4 years
wshadow141fix wshadow group 141Andres Noetzli4 years
wshadowNodeManagerFixed shadow warnings for batch number 14Andres Noetzli4 years
 
TagDownloadAuthorAge
test-tag2commit 0d51f9839e...Andrew Reynolds3 years
smtcomp2015-experimentalcommit ff5745a9f6...Kshitij Bansal9 years
smtcomp2015-stablecommit 9b32405be8...Kshitij Bansal9 years
1.4commit c0258d642d...Morgan Deters10 years
smtcomp2014-resubmissioncommit 15a15f5c9f...Tim King10 years
smtcomp2014-applicationcommit 933a5122ca...Morgan Deters10 years
smtcomp2014commit 44fde647e6...Morgan Deters10 years
1.3commit 97d7c35cb2...Morgan Deters10 years
casc24commit 4e32479206...Morgan Deters11 years
1.2commit 1ef3bf7434...Morgan Deters11 years
smteval2013commit 843cfdae17...Morgan Deters11 years
1.1commit 92058c8c7a...Morgan Deters11 years
smtcomp2012-resubmission-2commit 7fcf0cb48a...François Bobot11 years
smtcomp2012-resubmissioncommit 2f282e67ed...François Bobot11 years
1.0commit b1556c088e...Morgan Deters11 years
smtcomp2012commit eaa2d2f431...Morgan Deters12 years
smtcomp2010commit 6c68124e7f...Morgan Deters14 years
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback