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
path:
root
/
test
/
regress
/
regress0
Mode
Name
Size
d---------
arith
1963
log
plain
-rw-r--r--
arr1.smt2
260
log
plain
-rw-r--r--
arr1.smtv1.smt2
295
log
plain
-rw-r--r--
arr2.smtv1.smt2
337
log
plain
-rw-r--r--
array-const-real-parse.smt2
232
log
plain
-rw-r--r--
arrayinuf_declare.smt2
97
log
plain
d---------
arrays
1595
log
plain
d---------
aufbv
2328
log
plain
d---------
auflia
558
log
plain
d---------
bool
42
log
plain
-rw-r--r--
boolean-prec.cvc
157
log
plain
-rw-r--r--
boolean-terms-bug-array.smt2
181
log
plain
-rw-r--r--
boolean-terms-kernel1.smt2
300
log
plain
-rw-r--r--
boolean-terms.cvc
254
log
plain
-rw-r--r--
bt-test-00.smt2
395
log
plain
-rw-r--r--
bt-test-01.smt2
422
log
plain
-rw-r--r--
bug1247.smt2
278
log
plain
-rw-r--r--
bug161.smtv1.smt2
158
log
plain
-rw-r--r--
bug164.smtv1.smt2
286
log
plain
-rw-r--r--
bug167.smtv1.smt2
465
log
plain
-rw-r--r--
bug168.smtv1.smt2
142
log
plain
-rw-r--r--
bug187.smt2
123
log
plain
-rw-r--r--
bug217.smt2
344
log
plain
-rw-r--r--
bug220.smt2
17
log
plain
-rw-r--r--
bug239.smtv1.smt2
3635
log
plain
-rw-r--r--
bug274.cvc
1553
log
plain
-rw-r--r--
bug288.smtv1.smt2
160
log
plain
-rw-r--r--
bug288b.smtv1.smt2
166
log
plain
-rw-r--r--
bug288c.smtv1.smt2
215
log
plain
-rw-r--r--
bug303.smt2
461
log
plain
-rw-r--r--
bug310.cvc
127
log
plain
-rw-r--r--
bug32.cvc
68
log
plain
-rw-r--r--
bug322.cvc
998
log
plain
-rw-r--r--
bug322b.cvc
242
log
plain
-rw-r--r--
bug339.smt2
203
log
plain
-rw-r--r--
bug365.smt2
149
log
plain
-rw-r--r--
bug382.smt2
339
log
plain
-rw-r--r--
bug383.smt2
159
log
plain
-rw-r--r--
bug398.smt2
60
log
plain
-rw-r--r--
bug421.smt2
309
log
plain
-rw-r--r--
bug421b.smt2
502
log
plain
-rw-r--r--
bug480.smt2
312
log
plain
-rw-r--r--
bug484.smt2
1926
log
plain
-rw-r--r--
bug486.cvc
640
log
plain
-rw-r--r--
bug49.smtv1.smt2
2428
log
plain
-rw-r--r--
bug512.minimized.smt2
218
log
plain
-rw-r--r--
bug521.minimized.smt2
1887
log
plain
-rw-r--r--
bug522.smt2
200
log
plain
-rw-r--r--
bug528a.smt2
174
log
plain
-rw-r--r--
bug541.smt2
192
log
plain
-rw-r--r--
bug544.smt2
250
log
plain
-rw-r--r--
bug548a.smt2
392
log
plain
-rw-r--r--
bug576.smt2
769
log
plain
-rw-r--r--
bug576a.smt2
1841
log
plain
-rw-r--r--
bug578.smt2
187
log
plain
-rw-r--r--
bug586.cvc
533
log
plain
-rw-r--r--
bug595.cvc
103
log
plain
-rw-r--r--
bug596.cvc
111
log
plain
-rw-r--r--
bug596b.cvc
93
log
plain
-rw-r--r--
bug605.cvc
586
log
plain
-rw-r--r--
bug639.smt2
858
log
plain
-rw-r--r--
buggy-ite.smt2
355
log
plain
d---------
bv
6714
log
plain
-rw-r--r--
chained-equality.smt2
208
log
plain
-rw-r--r--
constant-rewrite.smtv1.smt2
184
log
plain
-rw-r--r--
cvc-rerror-print.cvc
205
log
plain
-rw-r--r--
cvc3-bug15.cvc
199
log
plain
-rw-r--r--
cvc3.userdoc.01.cvc
632
log
plain
-rw-r--r--
cvc3.userdoc.02.cvc
160
log
plain
-rw-r--r--
cvc3.userdoc.03.cvc
200
log
plain
-rw-r--r--
cvc3.userdoc.04.cvc
145
log
plain
-rw-r--r--
cvc3.userdoc.05.cvc
243
log
plain
-rw-r--r--
cvc3.userdoc.06.cvc
198
log
plain
d---------
datatypes
3318
log
plain
d---------
decision
821
log
plain
-rw-r--r--
declare-fun-is-match.smt2
217
log
plain
-rw-r--r--
declare-funs.smt2
103
log
plain
-rw-r--r--
define-fun-model.smt2
397
log
plain
-rw-r--r--
distinct.smtv1.smt2
257
log
plain
-rw-r--r--
dump-unsat-core-full.smt2
263
log
plain
-rw-r--r--
eqrange1.smt2
608
log
plain
-rw-r--r--
eqrange2.smt2
404
log
plain
-rw-r--r--
eqrange3.smt2
489
log
plain
d---------
expect
239
log
plain
-rw-r--r--
flet.smtv1.smt2
204
log
plain
-rw-r--r--
flet2.smtv1.smt2
190
log
plain
d---------
fmf
1264
log
plain
d---------
fp
488
log
plain
-rw-r--r--
fuzz_1.smtv1.smt2
849
log
plain
-rw-r--r--
fuzz_3.smtv1.smt2
652
log
plain
-rw-r--r--
get-value-incremental.smt2
304
log
plain
-rw-r--r--
get-value-ints.smt2
388
log
plain
-rw-r--r--
get-value-reals-ints.smt2
854
log
plain
-rw-r--r--
get-value-reals.smt2
607
log
plain
d---------
ho
1666
log
plain
-rw-r--r--
hung10_itesdk_output1.smt2
920
log
plain
-rw-r--r--
hung13sdk_output1.smt2
425
log
plain
-rw-r--r--
incorrect1.smtv1.smt2
1450
log
plain
-rw-r--r--
ineq_basic.smtv1.smt2
152
log
plain
-rw-r--r--
ineq_slack.smtv1.smt2
193
log
plain
-rw-r--r--
issue1063-overloading-dt-cons.smt2
439
log
plain
-rw-r--r--
issue1063-overloading-dt-fun.smt2
302
log
plain
-rw-r--r--
issue1063-overloading-dt-sel.smt2
296
log
plain
-rw-r--r--
issue2832-qualId.smt2
295
log
plain
-rw-r--r--
issue4010-sort-inf-var.smt2
151
log
plain
-rw-r--r--
issue4469-unc-no-reuse-var.smt2
190
log
plain
-rw-r--r--
issue4707-bv-to-bool-small.smt2
655
log
plain
-rw-r--r--
issue5099-model-1.smt2
219
log
plain
-rw-r--r--
issue5099-model-2.smt2
200
log
plain
-rw-r--r--
issue5144-resetAssertions.smt2
90
log
plain
-rw-r--r--
issue5187-div-justification.smt2
617
log
plain
-rw-r--r--
issue5370.smt2
585
log
plain
-rw-r--r--
issue5462.smt2
1318
log
plain
-rw-r--r--
issue5540-2-dump-model.smt2
195
log
plain
-rw-r--r--
issue5540-model-decls.smt2
355
log
plain
-rw-r--r--
issue5550-num-children.smt2
111
log
plain
-rw-r--r--
ite.cvc
79
log
plain
-rw-r--r--
ite.smt2
152
log
plain
-rw-r--r--
ite2.smt2
138
log
plain
-rw-r--r--
ite3.smt2
199
log
plain
-rw-r--r--
ite4.smt2
197
log
plain
-rw-r--r--
ite_arith.smt2
140
log
plain
-rw-r--r--
ite_real_int_type.smtv1.smt2
244
log
plain
-rw-r--r--
ite_real_valid.smtv1.smt2
195
log
plain
-rw-r--r--
lang_opts_2_6_1.smt2
249
log
plain
d---------
lemmas
269
log
plain
-rw-r--r--
let.cvc
101
log
plain
-rw-r--r--
let.smtv1.smt2
234
log
plain
-rw-r--r--
let2.smtv1.smt2
197
log
plain
-rw-r--r--
logops.01.cvc
89
log
plain
-rw-r--r--
logops.02.cvc
60
log
plain
-rw-r--r--
logops.03.cvc
104
log
plain
-rw-r--r--
logops.04.cvc
70
log
plain
-rw-r--r--
logops.05.cvc
61
log
plain
-rw-r--r--
model-core.smt2
305
log
plain
-rw-r--r--
models-print-1.smt2
254
log
plain
-rw-r--r--
models-print-2.smt2
383
log
plain
-rw-r--r--
named-expr-use.smt2
205
log
plain
d---------
nl
1606
log
plain
-rw-r--r--
opt-abd-no-use.smt2
129
log
plain
d---------
options
45
log
plain
-rw-r--r--
parallel-let.smt2
184
log
plain
d---------
parser
809
log
plain
d---------
precedence
726
log
plain
d---------
preprocess
887
log
plain
-rw-r--r--
print_define_fun_internal.smt2
289
log
plain
-rw-r--r--
print_lambda.cvc
308
log
plain
-rw-r--r--
print_model.cvc
236
log
plain
d---------
printer
337
log
plain
d---------
push-pop
834
log
plain
d---------
quantifiers
3782
log
plain
-rw-r--r--
rec-fun-const-parse-bug.smt2
197
log
plain
d---------
rels
2588
log
plain
d---------
sep
703
log
plain
d---------
seq
1036
log
plain
d---------
sets
2118
log
plain
-rw-r--r--
simple-dump-model.smt2
285
log
plain
-rw-r--r--
simple-lra.smt2
174
log
plain
-rw-r--r--
simple-lra.smtv1.smt2
216
log
plain
-rw-r--r--
simple-rdl.smt2
147
log
plain
-rw-r--r--
simple-rdl.smtv1.smt2
184
log
plain
-rw-r--r--
simple-uf.smt2
201
log
plain
-rw-r--r--
simple-uf.smtv1.smt2
256
log
plain
-rw-r--r--
simple.cvc
136
log
plain
-rw-r--r--
simple.smtv1.smt2
285
log
plain
-rw-r--r--
simple2.smtv1.smt2
277
log
plain
-rw-r--r--
simplification_bug.smtv1.smt2
139
log
plain
-rw-r--r--
simplification_bug2.smtv1.smt2
168
log
plain
-rw-r--r--
smallcnf.cvc
143
log
plain
-rw-r--r--
smt2output.smt2
375
log
plain
d---------
smtlib
749
log
plain
d---------
strings
3880
log
plain
d---------
sygus
1656
log
plain
-rw-r--r--
symmetric.smtv1.smt2
249
log
plain
-rw-r--r--
test11.cvc
88
log
plain
-rw-r--r--
test9.cvc
65
log
plain
d---------
tptp
1330
log
plain
d---------
uf
1776
log
plain
-rw-r--r--
uf20-03.cvc
3395
log
plain
d---------
uflia
983
log
plain
d---------
uflra
1107
log
plain
d---------
unconstrained
1995
log
plain
-rw-r--r--
wiki.01.cvc
78
log
plain
-rw-r--r--
wiki.02.cvc
82
log
plain
-rw-r--r--
wiki.03.cvc
64
log
plain
-rw-r--r--
wiki.04.cvc
66
log
plain
-rw-r--r--
wiki.05.cvc
67
log
plain
-rw-r--r--
wiki.06.cvc
67
log
plain
-rw-r--r--
wiki.07.cvc
87
log
plain
-rw-r--r--
wiki.08.cvc
88
log
plain
-rw-r--r--
wiki.09.cvc
57
log
plain
-rw-r--r--
wiki.10.cvc
68
log
plain
-rw-r--r--
wiki.11.cvc
59
log
plain
-rw-r--r--
wiki.12.cvc
60
log
plain
-rw-r--r--
wiki.13.cvc
63
log
plain
-rw-r--r--
wiki.14.cvc
63
log
plain
-rw-r--r--
wiki.15.cvc
65
log
plain
-rw-r--r--
wiki.16.cvc
68
log
plain
-rw-r--r--
wiki.17.cvc
65
log
plain
-rw-r--r--
wiki.18.cvc
65
log
plain
-rw-r--r--
wiki.19.cvc
79
log
plain
-rw-r--r--
wiki.20.cvc
79
log
plain
-rw-r--r--
wiki.21.cvc
62
log
plain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback