index
:
cvc5.git
1.0.x
1.1.x
1.2.x
1.3.x
1.4.x
CIAddFlex
abstractVals
abstractValsPR
actions-ci-pr
addLemmas
addVerifyTests
aggCDSimp
aggSkolemSharing
aggSkolemSharingAlt
alwaysDeleteProofFiles
an/refactor/NodeBuilder
anonStrPR
anonymizeStrings
archiveRunScripts
arr_rewriter_refactor
arrayConst
assignment3
betterSkolems2
betterStripSymbolicLength
bidirQuantInst
bogusAssertions
bool-terms-with-skolems
boolean-term-reorg
braced-init-list
cacheReplSkolems
cav2019strings
cav2019strings_countRewRed
cav2019strings_exp
cav2020
cav2020submission
cav22-strings
changeAssoc
changeReg
check_exceptions
clang-tidy
clean_includes
cleanup_output
codeString
compiler_info
countRewRed
coverity1473023
createCheckEntailContains
cxxtest_pkg
d_slow_reg
dedup_lang
deleteInvalidMkConst
devel
differentIndexHeuristic
disableAggRegex
divModSem
div_semantics
doc
docsLink
dsl
duplicate_lemmas
eatmydata
emptyEq
emptyStrRewrites
eqNotifyRewrite
esolverPrototype
eval
eval3
eval4
eval5
eval6
evalStrCode
eval_fp
experiment
experimental
exprManagerConstrPrivate
ext_dec
extfSubst
fasterCompilation
finalOpts
fix-cln-static-download
fix1649
fix2002
fix2982
fix3020
fix3089
fix3475
fix3683
fix3959
fix3991
fix4376
fix4477
fix4644
fix4658
fix4771
fix5024
fix5090
fix6520
fix6639
fix7017
fixABC
fixANTLR
fixANTLRBuild
fixAmazon
fixArithLemmas
fixArithLemmasPR
fixAsan
fixAsanInteractiveShellBlack
fixBetterSkolems
fixBias
fixCI
fixCMSBuild
fixCMSBuildPR
fixClangWarnings
fixCollectEmptyEqs
fixConfigureTypo
fixDestrOrder
fixDump
fixEagerModels
fixErrorSet
fixEvalIdOf
fixExamples
fixExportTo
fixExtraVersion
fixFPbool
fixGetUnsatAssumptDump
fixGlpkBuild
fixInConflict
fixIssue3596
fixIssue5074
fixJavaConfig
fixJavaTests
fixLib64
fixLineNrWarns
fixLinking
fixMacBuild
fixMacOsAction
fixMemLeak
fixNightlies
fixNightliesNoProof
fixNightlyAsan
fixNightlyComp
fixNodeTraversal
fixNonDumping
fixOptionsDep
fixPPDumpPR
fixPPreg
fixPR2737
fixParseOnly
fixPayloadSeen
fixPoly
fixPrinter
fixRefCountZero
fixReg
fixRegNightlies
fixRegression4971
fixRevInference
fixSetInfoName
fixSolverBlackAmbiguity
fixStaticInstall
fixStrLitParser
fixStrRegress
fixStrictParsing
fixStrictParsingBvOp
fixTearDownIncremental
fixWShadow
fixWinBuild
fixWinTypes
fix_cdlist
fix_cmm_unit_test
fix_dist_build2
fix_eqproof
fix_java_tests
fix_lfsc_mem_leaks
fix_mem_leaks
fix_proof_spaces
fix_rewrite
fix_runscript
fix_sat_solver
fix_shared_win
fix_typos
fix_unsat_cores
fix_warns
fix_win_gmp
fmcad2020-strings
fp_to_ieee_bv
from_master_fix_compile_speed
from_master_fix_lfsc_leaks
ghActions
google
hack
ijcar2020
ijcar2020_cr
inc-adj-list
includes
incremental-adj-for-dirty
incremental-adjacent-try3
incremental-current-best
incremental-no-hashmap
indexof_re
ineq_assumptions
inferZero
input-parser
issue4028
issue4070
issue4077
issue4151
issue4367
issue4576
issue5330
issue6453
issue6636
issue6643
issue6661
issue6717
issue6834
issue7056
issue7504
issue7569
kindSkolems
lenInConc
lengthPreserve
leqRew
lessRewrites
lfscTests
libdir
link_smt
m1build
macos11
mapConstRational
master
matthew-bellman-non-inc
mergePostSuffix
mergePostSuffix2
miscWarns
mkExceptionPublic
moveDetectLoop
moveKinded
moveSlowReg
move_constr
move_visitor
mpfr
mult_args
multiple-cycles-quick
newApiForCommands
newCtnInf
newCtnR
newSubstr
newl
next_model_cherry_fix
noNormalLoopBreak
nodeArrayStoreAll
nodeAssertionList
nodeEmptySet
nodeEmptySetPR
nodeUConst
nodeView
normalFormsHeuristic
normalFormsHeuristic2
normalizeStringsSkolemAgg
notCtnRed
nproc
oldVarHeuristic
oldVarHeuristicPR
oneWeirdRewrite
optExp
optNormalForm
optStringHash
optimizeRunscriptSLIA
overlap
parser-state
paserNamedErrorMsg
pldi2019
postrelease
prePostKinds
prefixes
pri_user_lang
printHistogramKinds
privateGet
projIssue316
projIssue327
projIssue340
proof-new-dsl
python3.5reg
quantifier_proofs
quantifier_proofs_
quickLenConflict
reAllSupport
reAllSupport2
reElimChange
reInterRew
reLoopRew
recordAssumptions
reduceReplacePR
reenableContextBlack
reenableSSCombine
refactorArrayCoreSolver
refactorEagerSolver
refactorProcessSimpleDeq
refactorProcessSimpleDeqPR
refactorTheoryBoolRewriter
refactorUnconstrainedSimp
refactor_pp
refactor_pp_backup
refactor_pp_registry
regDisableProofs
regWDefaultCmdLine
regexRRVerify
regexpBidirUnfold
remove-cd-dense-set
removeBinaryCsp
removeBinaryCspPR
remove_in_assertions
remove_throw
renameJavaPackage
replSubst
replaceReplace
replaceRewrites
replaceRewritesCache
replaceSubstitute
replace_re
replreplRew
revIter
reverseSkolemMap
revertMoveSSCombine
rewContains
rewContainsPR
rewIndexOf
rewInfer
rewriteREtoContains
rewrite_concat
rewrite_proof
rewrite_proof_test
rm-bv-div-zero-const-refs
rmAliases
rmBindingsParser
rmCDAttr
rmCoverity
rmExprSequence
rmHeuristic
rmMaybe
rmNoInteractivePrompt
rmOutdated
rmPostsolve
rmStateOptions
rmStatic
rmTearDownIncremental
rmUnusedNmFns
rm_cd_set_collection
rm_cdchunklist2
rm_cdvector
rm_invalid_reg
rm_svn
rm_tls
run_new_logics
safePrintInferences
sat2019
sendExplLemma
skipReg
smtcomp2019_fixed
smtcomp2020starexec
smtcomp2021
smtcomp2021-fixed
smtcompopts
solveEqRew
splitEqLen
splitEqRew
starter-bellman-inc
starter-inc-longs
starterProject
stdAttrs
strRewrites
stratRe-062019_exp
stringReplaceUsingIndexOf
stringsPfFixCycleDetect
stringsPfRewriterPR
stringsSkolemLenFix
strongerContainsRew
subsolverParams
substrsubstr
summary_folders
sygus2018stringsRew
test
theoryElimContext
theoryRewriters
travis_timing
udiv_const
ufSkolems
unordered_maps_pull_request_fix
unsat_assum_reg
unsat_core_example
up-fix-fix
update1.9news
updateCvc5h
updateLangHelp
updateRunScripts
updateScripts
warn_spaces
weakenCheckUnsatCore
win_deps_tmp
wshadow
wshadow141
wshadowNodeManager
CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
git repository hosting
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Branch
Commit message
Author
Age
1.0.x
fix up build system for swig (d242c30 introduced a subtle error)
Morgan Deters
12 years
1.1.x
bug 374 fix: assert litVal=desiredVal only for leaf nodes
Kshitij Bansal
11 years
1.2.x
bug 374 fix: assert litVal=desiredVal only for leaf nodes
Kshitij Bansal
11 years
1.3.x
Fixing bug 552. There was a bug when integers are made using a string with a...
Tim King
11 years
1.4.x
remove options infrastructure code which depended on undefined behavior
Kshitij Bansal
9 years
CIAddFlex
[CI] Update package list
Andres Noetzli
4 years
abstractVals
Unify abstract values and uninterpreted constants
Andres Noetzli
3 years
abstractValsPR
Unify abstract values and uninterpreted constants
Andres Noetzli
3 years
actions-ci-pr
Make a unit test fail
Andres Noetzli
5 years
addLemmas
replace lemma
Andres Noetzli
5 years
addVerifyTests
Merge branch 'master' into addVerifyTests
Andrew Reynolds
6 years
aggCDSimp
Aggressive CD simplifications
Andres Noetzli
4 years
aggSkolemSharing
Merge branch 'revertMoveSSCombine' into aggSkolemSharing
Andres Noetzli
6 years
aggSkolemSharingAlt
minor
Andres Noetzli
6 years
alwaysDeleteProofFiles
Delete temporary proof files when aborting CVC4
Andres Noetzli
6 years
an/refactor/NodeBuilder
Remove template argument from `NodeBuilder`
Andres Noetzli
3 years
anonStrPR
remove experiments
Andres Noetzli
5 years
anonymizeStrings
remove experiments
Andres Noetzli
5 years
archiveRunScripts
Merge branch 'master' into archiveRunScripts
Mathias Preiner
3 years
arr_rewriter_refactor
Move array rewriter functions to source file
Andres Notzli
8 years
arrayConst
Faster isConst
Andres Noetzli
3 years
assignment3
Fix edge direction
Andres Noetzli
5 years
betterSkolems2
minor
Andres Noetzli
6 years
betterStripSymbolicLength
update
Andres Noetzli
6 years
bidirQuantInst
Bidirectional quantifier instantiation
Andres Noetzli
5 years
bogusAssertions
Fix bogus assertions
Andres Noetzli
5 years
bool-terms-with-skolems
todo
Dejan Jovanovic
9 years
boolean-term-reorg
another test case
Dejan Jovanovic
9 years
braced-init-list
Merge branch 'master' into braced-init-list
Andres Noetzli
3 years
cacheReplSkolems
Cache replace skolems
Andres Noetzli
6 years
cav2019strings
Add counter
Andres Noetzli
5 years
cav2019strings_countRewRed
merge
Andres Noetzli
5 years
cav2019strings_exp
new rewrite
Andres Noetzli
5 years
cav2020
Length requirements in conclusions
Andres Noetzli
5 years
cav2020submission
Stats per skolem id
Andres Noetzli
5 years
cav22-strings
Merge branch 'master' into cav22-strings
Andrew Reynolds
3 years
changeAssoc
Change FlattenAssocCommut rewrite
Andres Noetzli
5 years
changeReg
Strings: Register skolems before sending lemma
Andres Noetzli
4 years
check_exceptions
Add check for C++ exceptions to config script
Andres Notzli
7 years
clang-tidy
test2
Andres Noetzli
4 years
clean_includes
more cleanup
Andres Noetzli
7 years
cleanup_output
Merge branch 'master' into cleanup_output
Mathias Preiner
7 years
codeString
support for code.str
Andres Noetzli
5 years
compiler_info
fix
Andres Noetzli
6 years
countRewRed
fix
Andres Noetzli
6 years
coverity1473023
Merge branch 'master' into coverity1473023
Andres Noetzli
6 years
createCheckEntailContains
Merge branch 'master' into createCheckEntailContains
Andrew Reynolds
6 years
cxxtest_pkg
Add cxxtest as package
Andres Notzli
7 years
d_slow_reg
Merge branch 'master' into d_slow_reg
Andres Noetzli
6 years
dedup_lang
Formatting
Andres Noetzli
6 years
deleteInvalidMkConst
Merge branch 'master' into deleteInvalidMkConst
Andrew Reynolds
3 years
devel
Re-enabling properConflict assertion
Clark Barrett
9 years
differentIndexHeuristic
Different heuristic
Andres Noetzli
5 years
disableAggRegex
disable agg regex
Andres Noetzli
5 years
divModSem
Merge branch 'master' into divModSem
Aina Niemetz
4 years
div_semantics
Merge branch 'master' into div_semantics
Andrew Reynolds
7 years
doc
Merge branch 'master' into doc
Aina Niemetz
4 years
docsLink
Merge branch 'master' into docsLink
Andres Noetzli
3 years
dsl
verification
Andres Noetzli
3 years
duplicate_lemmas
backjumping to make propagation lemmas current
Dejan Jovanovic
8 years
eatmydata
quick test
Andres Noetzli
6 years
emptyEq
Merge branch 'master' into emptyEq
Andrew Reynolds
6 years
emptyStrRewrites
fix
Andres Noetzli
6 years
eqNotifyRewrite
lazy registration
Andres Noetzli
4 years
esolverPrototype
Protype e-solver implementation
Andres Noetzli
3 years
eval
Fallback
Andres Noetzli
6 years
eval3
Evaluator: support other theories for equality
Andres Noetzli
6 years
eval4
Fix hanging evaluator
Andres Noetzli
6 years
eval5
Fix CONST_RATIONAL conversion in evaluation
Andres Noetzli
6 years
eval6
Evaluator: support and/or, contains, prefix/suffix
Andres Noetzli
6 years
evalStrCode
Merge branch 'master' into evalStrCode
Andrew Reynolds
6 years
eval_fp
Add floating-point support in evaluator
Andres Noetzli
6 years
experiment
Partial fix for bug 717.
Clark Barrett
7 years
experimental
Fixing cryptominisat build issues
Liana Hadarean
9 years
exprManagerConstrPrivate
Merge branch 'master' into exprManagerConstrPrivate
Andres Noetzli
4 years
ext_dec
Merge remote-tracking branch 'ajreynol/extDecomposeRevisit' into ext_dec
Andres Noetzli
6 years
extfSubst
More aggressive substitutions for extf eval
Andres Noetzli
4 years
fasterCompilation
Improve compile times
Andres Noetzli
6 years
finalOpts
Merge branch 'master' into finalOpts
Andres Noetzli
3 years
fix-cln-static-download
Merge branch 'master' into fix-cln-static-download
Andrew Reynolds
3 years
fix1649
Merge branch 'master' into fix1649
Gereon Kremer
3 years
fix2002
Merge branch 'master' into fix2002
Andres Noetzli
6 years
fix2982
Merge branch 'master' into fix2982
Andrew Reynolds
5 years
fix3020
Avoid substituting Boolean term variables
Andres Noetzli
5 years
fix3089
Merge branch 'master' into fix3089
Andrew Reynolds
5 years
fix3475
Merge branch 'master' into fix3475
Andrew Reynolds
5 years
fix3683
Fix arithmetic rewriter for exponential
Andres Noetzli
5 years
fix3959
Merge branch 'master' into fix3959
Andrew Reynolds
5 years
fix3991
Merge branch 'master' into fix3991
Andrew Reynolds
4 years
fix4376
Reinstantiate support for conjunctions in facts
Andres Noetzli
4 years
fix4477
Merge branch 'master' into fix4477
Andrew Reynolds
4 years
fix4644
[unconstrained] Fix gathering of visited-once vars
Andres Noetzli
4 years
fix4658
Fix memory leak in unit test node_algorithm_black
Andres Noetzli
4 years
fix4771
Fix 4771
Andres Noetzli
4 years
fix5024
Merge branch 'master' into fix5024
Andrew Reynolds
4 years
fix5090
Merge branch 'master' into fix5090
Andrew Reynolds
4 years
fix6520
Merge branch 'master' into fix6520
Mathias Preiner
3 years
fix6639
Merge branch 'master' into fix6639
Andrew Reynolds
3 years
fix7017
minor
Andres Noetzli
3 years
fixABC
Merge branch 'master' into fixABC
Andrew Reynolds
4 years
fixANTLR
Fix `ANTLR3_COMMAND` for system ANTLR3 JAR
Andres Noetzli
3 years
fixANTLRBuild
Merge branch 'master' into fixANTLRBuild
Andres Noetzli
3 years
fixAmazon
Fix linking ANTLR3 on some systems
Andres Noetzli
3 years
fixArithLemmas
Fix arith lemmas for mod/div
Andres Noetzli
4 years
fixArithLemmasPR
Fix Arith lemmas for div/mod
Andres Noetzli
4 years
fixAsan
fix
Andres Noetzli
6 years
fixAsanInteractiveShellBlack
Merge branch 'master' into fixAsanInteractiveShellBlack
Andrew Reynolds
4 years
fixBetterSkolems
Merge branch 'master' into fixBetterSkolems
Andres Noetzli
5 years
fixBias
Merge branch 'master' into fixBias
Alex Ozdemir
6 years
fixCI
[CI] Fix Cython installation
Andres Noetzli
4 years
fixCMSBuild
Fix CryptoMiniSat build, regression
Andres Noetzli
4 years
fixCMSBuildPR
Merge branch 'master' into fixCMSBuildPR
Andrew Reynolds
4 years
fixClangWarnings
Merge branch 'master' into fixClangWarnings
Andres Noetzli
4 years
fixCollectEmptyEqs
Merge branch 'master' into fixCollectEmptyEqs
Andres Noetzli
6 years
fixConfigureTypo
Merge branch 'master' into fixConfigureTypo
Aina Niemetz
6 years
fixDestrOrder
Merge branch 'master' into fixDestrOrder
Alex Ozdemir
6 years
fixDump
Merge branch 'master' into fixDump
Andres Noetzli
6 years
fixEagerModels
Merge branch 'master' into fixEagerModels
Aina Niemetz
5 years
fixErrorSet
Merge branch 'master' into fixErrorSet
Andrew Reynolds
3 years
fixEvalIdOf
Merge branch 'master' into fixEvalIdOf
Andrew Reynolds
6 years
fixExamples
Fix use of APPLY kind in examples
Andres Noetzli
5 years
fixExportTo
Merge branch 'master' into fixExportTo
Andrew Reynolds
6 years
fixExtraVersion
Merge branch 'master' into fixExtraVersion
Andrew Reynolds
4 years
fixFPbool
Fix fp-bool.sy grammar and require symfpu
Andres Noetzli
6 years
fixGetUnsatAssumptDump
Merge branch 'master' into fixGetUnsatAssumptDump
Aina Niemetz
6 years
fixGlpkBuild
Fix GLPK build on older CMake versions
Andres Noetzli
3 years
fixInConflict
Revert semantic change from refactoring
Andres Noetzli
5 years
fixIssue3596
Merge branch 'master' into fixIssue3596
Andrew Reynolds
5 years
fixIssue5074
Merge branch 'master' into fixIssue5074
Andrew Reynolds
4 years
fixJavaConfig
Merge branch 'master' into fixJavaConfig
Andres Noetzli
3 years
fixJavaTests
Merge branch 'master' into fixJavaTests
Aina Niemetz
4 years
fixLib64
update
Andres Noetzli
3 years
fixLineNrWarns
Merge branch 'master' into fixLineNrWarns
Andrew Reynolds
6 years
fixLinking
Merge branch 'master' into fixLinking
Andres Noetzli
3 years
fixMacBuild
Merge branch 'master' into fixMacBuild
Andres Noetzli
6 years
fixMacOsAction
Fix GitHub Actions macOS build
Andres Noetzli
3 years
fixMemLeak
Fix memory leak in unit test
Andres Noetzli
5 years
fixNightlies
Use uniform length limit for String constants
Andres Noetzli
6 years
fixNightliesNoProof
[Regressions] Require proof support for abduction
Andres Noetzli
5 years
fixNightlyAsan
C++ API: Fix OOB read in unit test
Andres Noetzli
6 years
fixNightlyComp
Merge branch 'master' into fixNightlyComp
Andrew Reynolds
4 years
fixNodeTraversal
Merge branch 'master' into fixNodeTraversal
Andrew Reynolds
4 years
fixNonDumping
Merge branch 'master' into fixNonDumping
Andres Noetzli
6 years
fixOptionsDep
Merge branch 'master' into fixOptionsDep
Andrew Reynolds
3 years
fixPPDumpPR
Fix dumping pre/post preprocessing passes
Andres Noetzli
6 years
fixPPreg
Merge branch 'master' into fixPPreg
Andrew Reynolds
6 years
fixPR2737
fix
Andres Noetzli
6 years
fixParseOnly
Merge branch 'master' into fixParseOnly
Andrew Reynolds
3 years
fixPayloadSeen
Fix redundant definitions of `NodeValue::getConst`
Andres Noetzli
3 years
fixPoly
Merge branch 'master' into fixPoly
Andres Noetzli
6 years
fixPrinter
Add support for printing `re.loop` and `re.^`
Andres Noetzli
4 years
fixRefCountZero
Merge branch 'master' into fixRefCountZero
Andrew Reynolds
5 years
fixReg
Merge branch 'master' into fixReg
Andres Noetzli
5 years
fixRegNightlies
Merge branch 'master' into fixRegNightlies
Andrew Reynolds
5 years
fixRegression4971
Make regression test `issue4971-0` more robust
Andres Noetzli
3 years
fixRevInference
Fix reverse inference
Andres Noetzli
5 years
fixSetInfoName
Merge branch 'master' into fixSetInfoName
Andrew Reynolds
6 years
fixSolverBlackAmbiguity
Merge branch 'master' into fixSolverBlackAmbiguity
Aina Niemetz
4 years
fixStaticInstall
Merge branch 'master' into fixStaticInstall
Andrew Reynolds
4 years
fixStrLitParser
Merge branch 'master' into fixStrLitParser
Andrew Reynolds
6 years
fixStrRegress
Merge branch 'master' into fixStrRegress
Andrew Reynolds
3 years
fixStrictParsing
Merge branch 'master' into fixStrictParsing
Aina Niemetz
6 years
fixStrictParsingBvOp
Merge branch 'master' into fixStrictParsingBvOp
Andres Noetzli
5 years
fixTearDownIncremental
Fix --tear-down-incremental
Andres Noetzli
3 years
fixWShadow
Merge branch 'master' into fixWShadow
Andres Noetzli
5 years
fixWinBuild
Merge branch 'master' into fixWinBuild
Andres Noetzli
3 years
fixWinTypes
Merge branch 'master' into fixWinTypes
Andrew Reynolds
4 years
fix_cdlist
Merge branch 'master' into fix_cdlist
Andres Noetzli
4 years
fix_cmm_unit_test
Merge branch 'master' into fix_cmm_unit_test
Andres Noetzli
7 years
fix_dist_build2
Fix typo in Makefile that makes distcheck fail
Andres Notzli
8 years
fix_eqproof
[LFSC] Fix memory leaks
Andres Noetzli
7 years
fix_java_tests
fix java tests
Andres Noetzli
7 years
fix_lfsc_mem_leaks
[LFSC] Fix memory leaks when creating CExprs
Andres Notzli
8 years
fix_mem_leaks
Avoid mixing new/delete with malloc/free
Andres Notzli
8 years
fix_proof_spaces
Fix missing/redundant spaces in proofs
Andres Notzli
8 years
fix_rewrite
Fix minor bug and typo in boolean rewriter
Andres Notzli
8 years
fix_runscript
Fix no-cbqi-innermost option name in run script
Andres Noetzli
6 years
fix_sat_solver
Fix
Andres Noetzli
6 years
fix_shared_win
Fix shared libraries for Windows build
Andres Notzli
8 years
fix_typos
Fix some typos, fix some formatting, minor cleanup
Andres Notzli
8 years
fix_unsat_cores
update run regression script
Andres Noetzli
7 years
fix_warns
Merge branch 'master' into fix_warns
Andres Noetzli
6 years
fix_win_gmp
Merge branch 'master' into fix_win_gmp
Andres Noetzli
7 years
fmcad2020-strings
Add skolem stats and sharing toggle
Andres Noetzli
4 years
fp_to_ieee_bv
Add support for fp.to_ieee_bv
Andres Noetzli
5 years
from_master_fix_compile_speed
fix
Andres Noetzli
7 years
from_master_fix_lfsc_leaks
[LFSC] Fix memory leaks related to IntExpr/RatExpr
Andres Noetzli
7 years
ghActions
Test
Andres Noetzli
4 years
google
Minor fixes for inst match generators. Updates to qip.
ajreynol
8 years
hack
bla
Andres Noetzli
5 years
ijcar2020
Option for toggling str.code
Andres Noetzli
5 years
ijcar2020_cr
Option for toggling str.code
Andres Noetzli
4 years
inc-adj-list
Revert "Slightly better sorting key"
Matthew Sotoudeh
3 years
includes
Merge branch 'master' into includes
Andrew Reynolds
3 years
incremental-adj-for-dirty
This seems to be the best of the past few commits
Matthew Sotoudeh
3 years
incremental-adjacent-try3
More like best than inc-adj
Matthew Sotoudeh
3 years
incremental-current-best
This seems to be the best of the past few commits
Matthew Sotoudeh
3 years
incremental-no-hashmap
Remove the rest of my CDHashMaps
Matthew Sotoudeh
3 years
indexof_re
Merge branch 'master' into indexof_re
Andrew Reynolds
3 years
ineq_assumptions
Merge branch 'master' into ineq_assumptions
Andrew Reynolds
7 years
inferZero
fix merge
Andres Noetzli
6 years
input-parser
Add new interface for parsing inputs
Andres Noetzli
3 years
issue4028
Merge branch 'master' into issue4028
Aina Niemetz
5 years
issue4070
Merge branch 'master' into issue4070
Andres Noetzli
5 years
issue4077
Merge branch 'master' into issue4077
Aina Niemetz
5 years
issue4151
Merge branch 'master' into issue4151
Aina Niemetz
5 years
issue4367
Merge branch 'master' into issue4367
Andrew Reynolds
4 years
issue4576
Merge branch 'master' into issue4576
Andrew Reynolds
4 years
issue5330
Merge branch 'master' into issue5330
Andrew Reynolds
4 years
issue6453
Merge branch 'master' into issue6453
Andrew Reynolds
3 years
issue6636
Merge branch 'master' into issue6636
Andres Noetzli
3 years
issue6643
Merge branch 'master' into issue6643
Mathias Preiner
3 years
issue6661
Merge branch 'master' into issue6661
Andrew Reynolds
3 years
issue6717
Merge branch 'master' into issue6717
Haniel Barbosa
3 years
issue6834
Merge branch 'master' into issue6834
Andrew Reynolds
3 years
issue7056
Merge branch 'master' into issue7056
Andres Noetzli
3 years
issue7504
Merge branch 'master' into issue7504
Gereon Kremer
3 years
issue7569
Merge branch 'master' into issue7569
Mathias Preiner
3 years
kindSkolems
more rewrites
Andres Noetzli
5 years
lenInConc
Move length requirements to conclusion
Andres Noetzli
5 years
lengthPreserve
Address comment
Andres Noetzli
6 years
leqRew
Merge branch 'master' into leqRew
Andrew Reynolds
4 years
lessRewrites
less rewrites
Andres Noetzli
6 years
lfscTests
Merge branch 'master' into lfscTests
Andrew Reynolds
4 years
libdir
ANTLR3: Install into `CMAKE_INSTALL_LIBDIR`
Andres Noetzli
3 years
link_smt
:link-smt
Andres Noetzli
7 years
m1build
Merge branch 'master' into m1build
Andres Noetzli
3 years
macos11
Merge branch 'master' into macos11
Andres Noetzli
3 years
mapConstRational
minor
Andres Noetzli
3 years
master
Fix `collectEmptyEqs()` in string utils
Andres Noetzli
3 years
matthew-bellman-non-inc
Update rewriter
Matthew Sotoudeh
3 years
mergePostSuffix
min
Andres Noetzli
6 years
mergePostSuffix2
nit
Andres Noetzli
6 years
miscWarns
Merge branch 'master' into miscWarns
Andrew Reynolds
6 years
mkExceptionPublic
Merge branch 'master' into mkExceptionPublic
Andres Noetzli
3 years
moveDetectLoop
Move detect loop
Andres Noetzli
6 years
moveKinded
Merge branch 'master' into moveKinded
Andrew Reynolds
6 years
moveSlowReg
Move slow string regression to regress3
Andres Noetzli
6 years
move_constr
implement move constructor for nodes
Andres Noetzli
7 years
move_visitor
Merge branch 'master' into move_visitor
Andrew Reynolds
6 years
mpfr
MPFR support
Andres Noetzli
6 years
mult_args
Merge branch 'master' into mult_args
Aina Niemetz
6 years
multiple-cycles-quick
Fix bugs in reporting multiple cycles
Matthew Sotoudeh
3 years
newApiForCommands
Sketch of refactoring the Commands to use new API
Andres Noetzli
6 years
newCtnInf
update
Andres Noetzli
6 years
newCtnR
Merge branch 'master' into newCtnR
Andrew Reynolds
6 years
newSubstr
New reduction for str.substr
Andres Noetzli
3 years
newl
Merge branch 'master' into newl
Andrew Reynolds
6 years
next_model_cherry_fix
Fix interface for bindings
Andres Noetzli
5 years
noNormalLoopBreak
no normal loop breaking
Andres Noetzli
6 years
nodeArrayStoreAll
Merge branch 'master' into nodeArrayStoreAll
Andrew Reynolds
4 years
nodeAssertionList
minor
Andres Noetzli
4 years
nodeEmptySet
Towards Node-level SmtEngine
Andres Noetzli
4 years
nodeEmptySetPR
Merge branch 'master' into nodeEmptySetPR
Andres Noetzli
4 years
nodeUConst
Merge branch 'master' into nodeUConst
Andrew Reynolds
4 years
nodeView
format
Andres Noetzli
3 years
normalFormsHeuristic
New normal forms heuristic
Andres Noetzli
5 years
normalFormsHeuristic2
Take into account exp size
Andres Noetzli
5 years
normalizeStringsSkolemAgg
minor
Andres Noetzli
6 years
notCtnRed
alt version
Andres Noetzli
6 years
nproc
Merge branch 'master' into nproc
Andres Noetzli
3 years
oldVarHeuristic
Prefer old variable heuristic
Andres Noetzli
5 years
oldVarHeuristicPR
Merge branch 'master' into oldVarHeuristicPR
Andrew Reynolds
5 years
oneWeirdRewrite
one weird rewrite
Andres Noetzli
6 years
optExp
optimize explanations
Andres Noetzli
4 years
optNormalForm
Minor optimization
Andres Noetzli
4 years
optStringHash
Faster hasing for `cvc5::String`
Andres Noetzli
3 years
optimizeRunscriptSLIA
Merge branch 'master' into optimizeRunscriptSLIA
Andrew Reynolds
5 years
overlap
experiment
Andres Noetzli
6 years
parser-state
Split parser state from parser class
Andres Noetzli
3 years
paserNamedErrorMsg
Merge branch 'master' into paserNamedErrorMsg
Andrew Reynolds
3 years
pldi2019
Move ss-combine rewrite to extended rewriter
Andres Noetzli
6 years
postrelease
Merge branch 'master' into postrelease
Andres Noetzli
4 years
prePostKinds
Merge branch 'revertMoveSSCombine' into prePostKinds
Andres Noetzli
6 years
prefixes
aggressive prefix deduction
Andres Noetzli
4 years
pri_user_lang
Merge branch 'master' into pri_user_lang
Andres Noetzli
6 years
printHistogramKinds
Merge branch 'master' into printHistogramKinds
Andrew Reynolds
4 years
privateGet
Merge branch 'master' into privateGet
Andrew Reynolds
3 years
projIssue316
Merge branch 'master' into projIssue316
Andrew Reynolds
3 years
projIssue327
[FP] Fix overly restrictive assertion
Andres Noetzli
3 years
projIssue340
Merge branch 'master' into projIssue340
Andrew Reynolds
3 years
proof-new-dsl
tmp
Andres Noetzli
3 years
python3.5reg
Merge branch 'master' into python3.5reg
Andrew Reynolds
3 years
quantifier_proofs
Support for quantifier proofs
Andres Noetzli
7 years
quantifier_proofs_
Support for quantifier proofs
Andres Noetzli
5 years
quickLenConflict
Detect conflict quickly
Andres Noetzli
5 years
reAllSupport
Merge branch 'master' into reAllSupport
Andrew Reynolds
5 years
reAllSupport2
minor
Andres Noetzli
5 years
reElimChange
Change re-elim
Andres Noetzli
4 years
reInterRew
Rewrites for re.inter
Andres Noetzli
5 years
reLoopRew
Rewrite for re.loop
Andres Noetzli
5 years
recordAssumptions
Record assumption info in AssertionPipeline
Andres Noetzli
6 years
reduceReplacePR
fix
Andres Noetzli
6 years
reenableContextBlack
Merge branch 'master' into reenableContextBlack
Andres Noetzli
3 years
reenableSSCombine
Reenable ss-combine
Andres Noetzli
6 years
refactorArrayCoreSolver
Merge branch 'master' into refactorArrayCoreSolver
Andrew Reynolds
3 years
refactorEagerSolver
Merge branch 'master' into refactorEagerSolver
Andrew Reynolds
3 years
refactorProcessSimpleDeq
Refactor CoreSolver::processSimpleDeq
Andres Noetzli
5 years
refactorProcessSimpleDeqPR
Merge branch 'master' into refactorProcessSimpleDeqPR
Andrew Reynolds
4 years
refactorTheoryBoolRewriter
Refactor TheoryBoolRewriter to use rewriter tables
Andres Noetzli
5 years
refactorUnconstrainedSimp
Merge branch 'master' into refactorUnconstrainedSimp
Andres Noetzli
6 years
refactor_pp
XExample for refactoring
Andres Notzli
7 years
refactor_pp_backup
fixed timer issue
Justin Xu
7 years
refactor_pp_registry
Initial work on PreprocessingPassRegistry
Andres Noetzli
7 years
regDisableProofs
Merge branch 'master' into regDisableProofs
Andrew Reynolds
4 years
regWDefaultCmdLine
Merge branch 'master' into regWDefaultCmdLine
Andrew Reynolds
5 years
regexRRVerify
Merge branch 'master' into regexRRVerify
Andrew Reynolds
6 years
regexpBidirUnfold
Unfold regexps two ways
Andres Noetzli
5 years
remove-cd-dense-set
Also remove cddense_set.h from the CMakeList
Matthew Sotoudeh
3 years
removeBinaryCsp
Remove `--strings-binary-csp` option
Andres Noetzli
5 years
removeBinaryCspPR
Remove `--strings-binary-csp` option
Andres Noetzli
5 years
remove_in_assertions
Remove input assertions
Andres Notzli
8 years
remove_throw
[Coverity] Remove throw qualifiers in src/smt
Andres Notzli
8 years
renameJavaPackage
Merge branch 'master' into renameJavaPackage
Andrew Reynolds
5 years
replSubst
address comment
Andres Noetzli
6 years
replaceReplace
fix comment
Andres Noetzli
6 years
replaceRewrites
Merge branch 'master' into replaceRewrites
Andrew Reynolds
6 years
replaceRewritesCache
skolem fns
Andres Noetzli
6 years
replaceSubstitute
Merge branch 'sygusComp2018-2' into replaceSubstitute
Andres Noetzli
6 years
replace_re
Add support for str.replace_re(_all)
Andres Noetzli
5 years
replreplRew
Merge branch 'master' into replreplRew
Andrew Reynolds
6 years
revIter
Merge branch 'master' into revIter
Andres Noetzli
3 years
reverseSkolemMap
contd
Andres Noetzli
5 years
revertMoveSSCombine
Revert "Move ss-combine rewrite to extended rewriter (#2703)"
Andres Noetzli
6 years
rewContains
test rewrite
Andres Noetzli
5 years
rewContainsPR
Merge branch 'master' into rewContainsPR
Andrew Reynolds
5 years
rewIndexOf
Strengthen str.indexof rewrite
Andres Noetzli
6 years
rewInfer
less aggressive
Andres Noetzli
6 years
rewriteREtoContains
Add rewrite for contains + const strings replace
Andres Noetzli
6 years
rewrite_concat
Merge branch 'master' into rewrite_concat
Andrew Reynolds
7 years
rewrite_proof
Support rewrite proofs in the theory of arrays
Andres Notzli
8 years
rewrite_proof_test
minor changes
Andres Noetzli
7 years
rm-bv-div-zero-const-refs
Merge branch 'master' into rm-bv-div-zero-const-refs
Andrew Reynolds
3 years
rmAliases
Merge branch 'master' into rmAliases
Andrew Reynolds
4 years
rmBindingsParser
fix
Andres Noetzli
5 years
rmCDAttr
Merge branch 'master' into rmCDAttr
Andres Noetzli
3 years
rmCoverity
Merge branch 'master' into rmCoverity
Aina Niemetz
6 years
rmExprSequence
Merge branch 'master' into rmExprSequence
Andrew Reynolds
4 years
rmHeuristic
Merge branch 'master' into rmHeuristic
Andrew Reynolds
5 years
rmMaybe
Merge branch 'master' into rmMaybe
Andrew Reynolds
3 years
rmNoInteractivePrompt
Merge branch 'master' into rmNoInteractivePrompt
Andrew Reynolds
3 years
rmOutdated
Merge branch 'master' into rmOutdated
Aina Niemetz
6 years
rmPostsolve
Remove unused postsolve infrastructure
Andres Noetzli
4 years
rmStateOptions
Merge branch 'master' into rmStateOptions
Andrew Reynolds
3 years
rmStatic
Remove static
Andres Noetzli
5 years
rmTearDownIncremental
Merge branch 'master' into rmTearDownIncremental
Andres Noetzli
3 years
rmUnusedNmFns
Merge branch 'master' into rmUnusedNmFns
Andrew Reynolds
3 years
rm_cd_set_collection
Merge branch 'master' into rm_cd_set_collection
Andres Noetzli
7 years
rm_cdchunklist2
Address Andy's comment
Andres Noetzli
7 years
rm_cdvector
Merge branch 'master' into rm_cdvector
Aina Niemetz
6 years
rm_invalid_reg
Merge branch 'master' into rm_invalid_reg
Andrew Reynolds
7 years
rm_svn
Merge branch 'master' into rm_svn
Andrew Reynolds
6 years
rm_tls
Merge branch 'master' into rm_tls
Andres Noetzli
6 years
run_new_logics
Merge branch 'master' into run_new_logics
Andrew Reynolds
6 years
safePrintInferences
Merge branch 'master' into safePrintInferences
Andrew Reynolds
5 years
sat2019
Move ss-combine rewrite to extended rewriter
Andres Noetzli
6 years
sendExplLemma
Send explanation lemma
Andres Noetzli
4 years
skipReg
Merge branch 'master' into skipReg
Andrew Reynolds
5 years
smtcomp2019_fixed
Avoid printing "success" for forced logic
Andres Noetzli
5 years
smtcomp2020starexec
[SMT-COMP] Redirect non-answers to /dev/null
Andres Noetzli
4 years
smtcomp2021
Final update to SMT-COMP 2021 options
Andres Noetzli
3 years
smtcomp2021-fixed
Add branch and bound lemma if linear arithmetic generates a non-integer assig...
Andrew Reynolds
3 years
smtcompopts
Merge branch 'master' into smtcompopts
Andrew Reynolds
3 years
solveEqRew
.
Andres Noetzli
6 years
splitEqLen
split len consts
Andres Noetzli
5 years
splitEqRew
Merge branch 'master' into splitEqRew
Andrew Reynolds
5 years
starter-bellman-inc
Remove the rest of my CDHashMaps
Matthew Sotoudeh
3 years
starter-inc-longs
Dirty nodes for the int64_t one
Matthew Sotoudeh
3 years
starterProject
Fix the rewriter
Matthew Sotoudeh
3 years
stdAttrs
Merge branch 'master' into stdAttrs
Mathias Preiner
3 years
strRewrites
Merge branch 'master' into strRewrites
Andrew Reynolds
6 years
stratRe-062019_exp
fix
Andres Noetzli
5 years
stringReplaceUsingIndexOf
Use str.indexof in str.replace reduction
Andres Noetzli
3 years
stringsPfFixCycleDetect
Fix detection of cyclic proofs
Andres Noetzli
4 years
stringsPfRewriterPR
Minor
Andres Noetzli
4 years
stringsSkolemLenFix
Protect length requirements
Andres Noetzli
5 years
strongerContainsRew
Minor
Andres Noetzli
6 years
subsolverParams
Merge branch 'master' into subsolverParams
Andres Noetzli
6 years
substrsubstr
Add length-based rewrites for (str.substr _ _ _)
Andres Noetzli
6 years
summary_folders
Restrict test summary to first-level subfolders
Andres Noetzli
6 years
sygus2018stringsRew
Merge branch 'master' into sygus2018stringsRew
Andrew Reynolds
6 years
test
test code
Andres Noetzli
7 years
theoryElimContext
Merge branch 'master' into theoryElimContext
Andres Noetzli
3 years
theoryRewriters
Address
Andres Noetzli
5 years
travis_timing
Travis timing
Andres Noetzli
7 years
udiv_const
minor fix
Andres Noetzli
7 years
ufSkolems
fix
Andres Noetzli
5 years
unordered_maps_pull_request_fix
also fix for tptp
Andres Noetzli
7 years
unsat_assum_reg
Merge branch 'master' into unsat_assum_reg
Aina Niemetz
7 years
unsat_core_example
example
Andres Notzli
8 years
up-fix-fix
Use TMPDIR environment variable for temp files
Andres Noetzli
6 years
update1.9news
Merge branch 'master' into update1.9news
Andrew Reynolds
4 years
updateCvc5h
[API] Update comments w.r.t. SymFPU
Andres Noetzli
3 years
updateLangHelp
Update `--lang=help`
Andres Noetzli
3 years
updateRunScripts
[SMT-COMP 2019] Update run scripts to match tracks
Andres Noetzli
5 years
updateScripts
Merge branch 'master' into updateScripts
Andres Noetzli
4 years
warn_spaces
Merge branch 'master' into warn_spaces
Andrew Reynolds
6 years
weakenCheckUnsatCore
Merge branch 'master' into weakenCheckUnsatCore
Andrew Reynolds
5 years
win_deps_tmp
remove exit
Andres Noetzli
7 years
wshadow
format
Andres Noetzli
5 years
wshadow141
fix wshadow group 141
Andres Noetzli
5 years
wshadowNodeManager
Fixed shadow warnings for batch number 14
Andres Noetzli
5 years
Tag
Download
Author
Age
test-tag2
commit 0d51f9839e...
Andrew Reynolds
3 years
smtcomp2015-experimental
commit ff5745a9f6...
Kshitij Bansal
9 years
smtcomp2015-stable
commit 9b32405be8...
Kshitij Bansal
9 years
1.4
commit c0258d642d...
Morgan Deters
10 years
smtcomp2014-resubmission
commit 15a15f5c9f...
Tim King
10 years
smtcomp2014-application
commit 933a5122ca...
Morgan Deters
10 years
smtcomp2014
commit 44fde647e6...
Morgan Deters
10 years
1.3
commit 97d7c35cb2...
Morgan Deters
11 years
casc24
commit 4e32479206...
Morgan Deters
11 years
1.2
commit 1ef3bf7434...
Morgan Deters
11 years
smteval2013
commit 843cfdae17...
Morgan Deters
11 years
1.1
commit 92058c8c7a...
Morgan Deters
11 years
smtcomp2012-resubmission-2
commit 7fcf0cb48a...
François Bobot
12 years
smtcomp2012-resubmission
commit 2f282e67ed...
François Bobot
12 years
1.0
commit b1556c088e...
Morgan Deters
12 years
smtcomp2012
commit eaa2d2f431...
Morgan Deters
12 years
smtcomp2010
commit 6c68124e7f...
Morgan Deters
14 years
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback