2024-04-23 20:03
ftp://ftp.de.debian.org/debian/pool/main/b/boolector/boolector_1.5.118.6b56be4.121013.orig.tar.gz
cppcheck-options: --library=posix --library=gnu  --check-library --inconclusive --enable=style,information --inline-suppr --disable=missingInclude --suppress=unmatchedSuppression --template=daca2 --debug-warnings --suppress=autoNoType --suppress=valueFlowBailout --suppress=bailoutUninitVar --suppress=symbolDatabaseWarning -D__GNUC__ --platform=unix64 -j2
platform: Linux-6.6.15-amd64-x86_64-with-glibc2.37
python: 3.11.8
client-version: 1.3.53
compiler: g++ (Debian 13.2.0-13) 13.2.0
cppcheck: head 2.14.0
head-info: 24be0e5 (2024-04-23 14:04:36 +0200)
count: 484 484
elapsed-time: 22.6 22.7
head-timing-info:

old-timing-info:

head results:
boolector-1.5.118-6b56be4-121013/btoraig.c:84:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:99:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:143:73: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:179:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable refs [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:200:54: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:334:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btoraig.c:1492:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cnf_id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:103:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:115:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:124:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:132:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:142:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:149:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:156:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:166:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:175:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:183:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:192:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:200:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:209:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:218:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:227:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:239:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:252:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:264:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:276:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:288:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:300:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:312:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:328:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:341:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:354:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:373:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:392:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:409:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:426:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:443:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:460:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:477:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:497:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:531:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:557:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:574:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:591:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:608:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:625:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:642:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:660:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:677:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:694:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:711:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:728:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:745:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:762:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:779:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:797:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:819:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:841:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:863:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:885:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:906:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:923:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:940:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:957:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:974:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:991:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1008:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1025:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1042:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1059:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1078:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1097:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1124:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1162:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1175:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1188:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1197:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1207:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1218:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1227:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1237:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1247:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1257:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1267:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1280:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1295:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1306:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1319:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1331:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1351:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/boolector.c:1216:54: style:inconclusive: Function 'boolector_get_symbol_of_var' argument 2 names different: declaration 'var' definition 'exp'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/boolector.h:893:66: note: Function 'boolector_get_symbol_of_var' argument 2 names different: declaration 'var' definition 'exp'.
boolector-1.5.118-6b56be4-121013/boolector.c:1216:54: note: Function 'boolector_get_symbol_of_var' argument 2 names different: declaration 'var' definition 'exp'.
boolector-1.5.118-6b56be4-121013/boolector.c:140:28: style: Parameter 'btor' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/boolector.c:494:13: style: Variable 'real_e0' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/boolector.c:494:23: style: Variable 'real_e1' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/boolector.c:529:13: style: Variable 'real_e0' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/boolector.c:529:23: style: Variable 'real_e1' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/boolector.c:1121:13: style: Variable 'real_e_if' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/boolector.c:1121:25: style: Variable 'real_e_else' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btoraig.c:700:45: style:inconclusive: Function 'btor_cond_aig' argument 2 names different: declaration 'aig_cond' definition 'a_cond'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:104:54: note: Function 'btor_cond_aig' argument 2 names different: declaration 'aig_cond' definition 'a_cond'.
boolector-1.5.118-6b56be4-121013/btoraig.c:700:45: note: Function 'btor_cond_aig' argument 2 names different: declaration 'aig_cond' definition 'a_cond'.
boolector-1.5.118-6b56be4-121013/btoraig.c:700:63: style:inconclusive: Function 'btor_cond_aig' argument 3 names different: declaration 'aig_if' definition 'a_if'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:104:74: note: Function 'btor_cond_aig' argument 3 names different: declaration 'aig_if' definition 'a_if'.
boolector-1.5.118-6b56be4-121013/btoraig.c:700:63: note: Function 'btor_cond_aig' argument 3 names different: declaration 'aig_if' definition 'a_if'.
boolector-1.5.118-6b56be4-121013/btoraig.c:701:9: style:inconclusive: Function 'btor_cond_aig' argument 4 names different: declaration 'aig_else' definition 'a_else'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:105:14: note: Function 'btor_cond_aig' argument 4 names different: declaration 'aig_else' definition 'a_else'.
boolector-1.5.118-6b56be4-121013/btoraig.c:701:9: note: Function 'btor_cond_aig' argument 4 names different: declaration 'aig_else' definition 'a_else'.
boolector-1.5.118-6b56be4-121013/btoraig.c:721:22: style:inconclusive: Function 'btor_dump_aigs' argument 3 names different: declaration 'output' definition 'file'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:123:27: note: Function 'btor_dump_aigs' argument 3 names different: declaration 'output' definition 'file'.
boolector-1.5.118-6b56be4-121013/btoraig.c:721:22: note: Function 'btor_dump_aigs' argument 3 names different: declaration 'output' definition 'file'.
boolector-1.5.118-6b56be4-121013/btoraig.c:723:22: style:inconclusive: Function 'btor_dump_aigs' argument 6 names different: declaration 'back_annotation' definition 'backannotation'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:125:27: note: Function 'btor_dump_aigs' argument 6 names different: declaration 'back_annotation' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btoraig.c:723:22: note: Function 'btor_dump_aigs' argument 6 names different: declaration 'back_annotation' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btoraig.c:756:23: style:inconclusive: Function 'btor_dump_aiger' argument 3 names different: declaration 'output' definition 'file'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:129:28: note: Function 'btor_dump_aiger' argument 3 names different: declaration 'output' definition 'file'.
boolector-1.5.118-6b56be4-121013/btoraig.c:756:23: note: Function 'btor_dump_aiger' argument 3 names different: declaration 'output' definition 'file'.
boolector-1.5.118-6b56be4-121013/btoraig.c:759:23: style:inconclusive: Function 'btor_dump_aiger' argument 9 names different: declaration 'back_annotation' definition 'backannotation'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:132:28: note: Function 'btor_dump_aiger' argument 9 names different: declaration 'back_annotation' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btoraig.c:759:23: note: Function 'btor_dump_aiger' argument 9 names different: declaration 'back_annotation' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btoraig.c:1202:55: style:inconclusive: Function 'btor_aig_to_sat_tseitin' argument 2 names different: declaration 'aig' definition 'start'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraig.h:146:60: note: Function 'btor_aig_to_sat_tseitin' argument 2 names different: declaration 'aig' definition 'start'.
boolector-1.5.118-6b56be4-121013/btoraig.c:1202:55: note: Function 'btor_aig_to_sat_tseitin' argument 2 names different: declaration 'aig' definition 'start'.
boolector-1.5.118-6b56be4-121013/btoraig.c:1088:28: style: Variable 'lr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btoraig.c:236:17: style: Variable 'temp' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btoraig.c:237:16: style: Variable 'cur' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btoraig.c:323:4: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btoraig.c:1397:3: style: Variable 'marked.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btoraig.c:1474:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btoraigvec.c:413:54: style:inconclusive: Function 'btor_mul_aigvec' argument 2 names different: declaration 'av1' definition 'a'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraigvec.h:125:66: note: Function 'btor_mul_aigvec' argument 2 names different: declaration 'av1' definition 'a'.
boolector-1.5.118-6b56be4-121013/btoraigvec.c:413:54: note: Function 'btor_mul_aigvec' argument 2 names different: declaration 'av1' definition 'a'.
boolector-1.5.118-6b56be4-121013/btoraigvec.c:413:70: style:inconclusive: Function 'btor_mul_aigvec' argument 3 names different: declaration 'av2' definition 'b'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btoraigvec.h:126:23: note: Function 'btor_mul_aigvec' argument 3 names different: declaration 'av2' definition 'b'.
boolector-1.5.118-6b56be4-121013/btoraigvec.c:413:70: note: Function 'btor_mul_aigvec' argument 3 names different: declaration 'av2' definition 'b'.
boolector-1.5.118-6b56be4-121013/btorbtor.c:91:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorbtor.c:355:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1859:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1810:3: style:inconclusive: Statements following 'return' will never be executed. [unreachableCode]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1683:51: style: Parameter 'opts' can be declared as pointer to const. However it seems that 'btor_new_btor_parser' is a callback function, if 'opts' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1969:20: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorbtor.c:1683:51: note: Parameter 'opts' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorbtor.c:1777:13: style: Variable 'e' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1281:17: error: Shifting signed 32-bit value by 31 bits is undefined behaviour [shiftTooManyBitsSigned]
boolector-1.5.118-6b56be4-121013/btorbtor.c:1278:3: note: After for loop, rlen has value 31
boolector-1.5.118-6b56be4-121013/btorbtor.c:1281:17: note: Shift
boolector-1.5.118-6b56be4-121013/btorbtor.c:1781:12: style: Variable 'e' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorconst.c:405:25: style: Redundant condition: The condition '*p' is redundant since '*p == '0'' is sufficient. [redundantCondition]
boolector-1.5.118-6b56be4-121013/btorconst.c:408:24: style: Redundant condition: The condition '*q' is redundant since '*q == '0'' is sufficient. [redundantCondition]
boolector-1.5.118-6b56be4-121013/btorconst.c:567:39: style:inconclusive: Function 'btor_decimal_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:44:45: note: Function 'btor_decimal_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:567:39: note: Function 'btor_decimal_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:596:37: style:inconclusive: Function 'btor_decimal_to_const' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:42:43: note: Function 'btor_decimal_to_const' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:596:37: note: Function 'btor_decimal_to_const' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:606:35: style:inconclusive: Function 'btor_hex_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:48:41: note: Function 'btor_hex_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:606:35: note: Function 'btor_hex_to_const_n' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:606:61: style:inconclusive: Function 'btor_hex_to_const_n' argument 3 names different: declaration 'len' definition 'hlen'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:48:67: note: Function 'btor_hex_to_const_n' argument 3 names different: declaration 'len' definition 'hlen'.
boolector-1.5.118-6b56be4-121013/btorconst.c:606:61: note: Function 'btor_hex_to_const_n' argument 3 names different: declaration 'len' definition 'hlen'.
boolector-1.5.118-6b56be4-121013/btorconst.c:740:33: style:inconclusive: Function 'btor_hex_to_const' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:46:39: note: Function 'btor_hex_to_const' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:740:33: note: Function 'btor_hex_to_const' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1497:50: style:inconclusive: Function 'btor_inverse_const' argument 2 names different: declaration 'a' definition 'c'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:92:57: note: Function 'btor_inverse_const' argument 2 names different: declaration 'a' definition 'c'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1497:50: note: Function 'btor_inverse_const' argument 2 names different: declaration 'a' definition 'c'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1559:33: style:inconclusive: Function 'btor_const_to_hex' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:123:40: note: Function 'btor_const_to_hex' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1559:33: note: Function 'btor_const_to_hex' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1609:37: style:inconclusive: Function 'btor_const_to_decimal' argument 1 names different: declaration 'mm' definition 'mem'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorconst.h:125:44: note: Function 'btor_const_to_decimal' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:1609:37: note: Function 'btor_const_to_decimal' argument 1 names different: declaration 'mm' definition 'mem'.
boolector-1.5.118-6b56be4-121013/btorconst.c:524:17: error: Shifting signed 32-bit value by 31 bits is undefined behaviour [shiftTooManyBitsSigned]
boolector-1.5.118-6b56be4-121013/btorconst.c:1654:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:179:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:186:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:196:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:218:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:255:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:281:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:293:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:936:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:166:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:191:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:213:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:256:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:274:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:293:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:312:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:331:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:353:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:384:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:402:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:484:4: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable prev_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:573:54: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:894:61: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:920:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable first_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:928:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable last_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:936:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable first_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:944:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable last_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:953:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable first_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:975:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable next_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:989:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable prev_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1003:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable next_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1015:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable prev_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1029:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable next_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1064:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1072:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1144:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1214:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1366:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1526:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1633:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable next_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1675:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable next_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1718:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable prev_aeq_acond_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1734:51: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1811:46: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1871:55: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1927:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:1944:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2011:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable prev_parent [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2030:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2067:45: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2169:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2195:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2225:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2286:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2320:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2356:44: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2680:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2741:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2782:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2794:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2809:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2819:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2838:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2848:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2858:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2868:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2878:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:2967:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3013:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3155:58: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3170:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3192:58: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3234:44: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3270:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3280:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3303:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3325:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3376:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3429:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3533:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3684:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3758:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3785:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3835:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3874:58: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3915:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:3957:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4060:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4074:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4086:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4095:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4104:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4116:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable symbol [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4299:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4469:58: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable id [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5088:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable __func__ [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5254:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5441:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5472:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5536:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable av [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5559:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5685:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tseitin [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:5931:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6002:58: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6078:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable av [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6121:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable av [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6222:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6863:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6918:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable constraint [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6934:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable constraint [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:6956:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7009:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7210:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7277:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7326:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7343:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7430:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:7972:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable constraint [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:8769:15: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:8861:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:8904:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorexp.c:4504:14: style: Redundant condition: e. '!e || (e && (e->kind)==BTOR_BV_VAR_NODE)' is equivalent to '!e || (e->kind)==BTOR_BV_VAR_NODE' [redundantCondition]
boolector-1.5.118-6b56be4-121013/btorexp.c:8186:16: style: Condition 's2->lower>s1->upper' is always false [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorexp.c:8185:50: note: Assuming that condition 's1->upper<s2->lower' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:8186:16: note: Condition 's2->lower>s1->upper' is always false
boolector-1.5.118-6b56be4-121013/btorexp.c:8200:13: style: Condition 'min==s1->lower' is always false [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorexp.c:8193:9: note: min is assigned '(s1->lower)<(s2->lower)?(s1->lower):(s2->lower)' here.
boolector-1.5.118-6b56be4-121013/btorexp.c:8200:13: note: Condition 'min==s1->lower' is always false
boolector-1.5.118-6b56be4-121013/btorexp.c:8223:13: style: Condition 'max==s1->upper' is always false [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorexp.c:8216:9: note: max is assigned '(s1->upper)>(s2->upper)?(s1->upper):(s2->upper)' here.
boolector-1.5.118-6b56be4-121013/btorexp.c:8223:13: note: Condition 'max==s1->upper' is always false
boolector-1.5.118-6b56be4-121013/btorexp.c:1108:10: warning: Either the condition 'exp' is redundant or there is possible null pointer dereference: exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:1110:11: note: Assuming that condition 'exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:1108:10: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:1984:7: warning: Either the condition 'parent' is redundant or there is possible null pointer dereference: parent. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:1986:12: note: Assuming that condition 'parent' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:1984:7: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:1993:7: warning: Either the condition 'parent' is redundant or there is possible null pointer dereference: parent. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:1986:12: note: Assuming that condition 'parent' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:1993:7: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:4443:15: warning: Either the condition 'e' is redundant or there is possible null pointer dereference: e. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:4445:11: note: Assuming that condition 'e' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:4443:15: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:4457:23: warning: Either the condition 'e' is redundant or there is possible null pointer dereference: e. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:4445:11: note: Assuming that condition 'e' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:4457:23: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:4491:38: warning: Either the condition 'e' is redundant or there is possible null pointer dereference: e. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:4488:11: note: Assuming that condition 'e' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:4491:38: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:4556:51: warning: Either the condition 'e' is redundant or there is possible null pointer dereference: e. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:4546:16: note: Assuming that condition 'e' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:4556:51: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5177:15: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5177:15: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5178:15: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5178:15: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5180:11: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5180:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5183:11: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5183:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5188:11: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5188:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5190:4: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5191:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5190:4: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5270:5: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5250:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5270:5: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5279:12: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5281:13: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5279:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5280:4: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5281:13: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5280:4: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5283:8: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5373:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5283:8: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5295:13: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5373:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5295:13: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5372:16: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5373:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5372:16: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5844:11: warning: Either the condition 'exp' is redundant or there is possible null pointer dereference: exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5850:7: note: Assuming that condition 'exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5844:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5846:12: warning: Either the condition 'exp' is redundant or there is possible null pointer dereference: exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5850:7: note: Assuming that condition 'exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5846:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:3: warning: Either the condition 'acc1' is redundant or there is possible null pointer dereference: acc1. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:3: note: Assuming that condition 'acc1' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:3: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:35: warning: Either the condition 'acc2' is redundant or there is possible null pointer dereference: acc2. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:35: note: Assuming that condition 'acc2' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5959:35: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:5983:31: warning: Either the condition 'acc' is redundant or there is possible null pointer dereference: acc. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:5983:31: note: Assuming that condition 'acc' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:5983:31: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6076:11: warning: Either the condition 'acc' is redundant or there is possible null pointer dereference: acc. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6076:11: note: Assuming that condition 'acc' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6076:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6170:15: warning: Either the condition 'acc' is redundant or there is possible null pointer dereference: acc. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6170:15: note: Assuming that condition 'acc' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6170:15: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6191:23: warning: Either the condition 'hashed_acc' is redundant or there is possible null pointer dereference: hashed_acc. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6191:23: note: Assuming that condition 'hashed_acc' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6191:23: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6260:15: warning: Either the condition 'array' is redundant or there is possible null pointer dereference: array. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6205:11: note: Assuming that condition 'array' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6260:15: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6262:38: warning: Either the condition 'array' is redundant or there is possible null pointer dereference: array. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6205:11: note: Assuming that condition 'array' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6262:38: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6299:17: warning: Either the condition 'next' is redundant or there is possible null pointer dereference: next. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6303:13: note: Assuming that condition 'next' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6299:17: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6300:12: warning: Either the condition 'next' is redundant or there is possible null pointer dereference: next. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6303:13: note: Assuming that condition 'next' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6300:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6330:17: warning: Either the condition 'next' is redundant or there is possible null pointer dereference: next. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6334:13: note: Assuming that condition 'next' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6330:17: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:6331:12: warning: Either the condition 'next' is redundant or there is possible null pointer dereference: next. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:6334:13: note: Assuming that condition 'next' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:6331:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7557:11: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7560:16: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7557:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7562:11: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7585:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7562:11: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7565:4: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7566:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7565:4: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7583:12: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7585:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7583:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7584:4: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7585:8: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7584:4: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7692:12: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7697:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7692:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7695:8: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7697:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7695:8: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:7751:12: warning: Either the condition 'cur' is redundant or there is possible null pointer dereference: cur. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:7754:12: note: Assuming that condition 'cur' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:7751:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:8918:14: warning: Either the condition 'real_exp' is redundant or there is possible null pointer dereference: real_exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:8909:7: note: Assuming that condition 'real_exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:8918:14: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:8973:12: warning: Either the condition '(struct BtorNode*)b->data.asPtr' is redundant or there is possible null pointer dereference: (struct BtorNode*)b->data.asPtr. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorexp.c:8973:12: note: Assuming that condition '(struct BtorNode*)b->data.asPtr' is not redundant
boolector-1.5.118-6b56be4-121013/btorexp.c:8973:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorexp.c:8082:21: style: Same expression on both sides of '=='. [duplicateExpression]
boolector-1.5.118-6b56be4-121013/btorexp.c:8185:63: style: Same expression on both sides of '||' because 's2->lower>s1->upper' and 's1->upper<s2->lower' represent the same value. [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorexp.c:8186:29: style: Same expression 's1->lower>s2->upper' found multiple times in chain of '||' operators because 's1->lower>s2->upper' and 's2->upper<s1->lower' represent the same value. [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorexp.c:4753:5: style:inconclusive: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak]
boolector-1.5.118-6b56be4-121013/btorexp.c:5177:31: style: Unsigned expression 'cur->synth_mark' can't be negative so it is unnecessary to test it. [unsignedPositive]
boolector-1.5.118-6b56be4-121013/btorexp.c:864:43: style:inconclusive: Function 'btor_release_exp' argument 2 names different: declaration 'exp' definition 'root'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorexp.h:859:48: note: Function 'btor_release_exp' argument 2 names different: declaration 'exp' definition 'root'.
boolector-1.5.118-6b56be4-121013/btorexp.c:864:43: note: Function 'btor_release_exp' argument 2 names different: declaration 'exp' definition 'root'.
boolector-1.5.118-6b56be4-121013/btorexp.c:2587:25: style:inconclusive: Function 'btor_int_to_exp' argument 1 names different: declaration 'emg' definition 'btor'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorexp.h:518:35: note: Function 'btor_int_to_exp' argument 1 names different: declaration 'emg' definition 'btor'.
boolector-1.5.118-6b56be4-121013/btorexp.c:2587:25: note: Function 'btor_int_to_exp' argument 1 names different: declaration 'emg' definition 'btor'.
boolector-1.5.118-6b56be4-121013/btorexp.c:4307:55: style:inconclusive: Function 'btor_dump_exps' argument 3 names different: declaration 'exps' definition 'roots'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorexp.h:863:60: note: Function 'btor_dump_exps' argument 3 names different: declaration 'exps' definition 'roots'.
boolector-1.5.118-6b56be4-121013/btorexp.c:4307:55: note: Function 'btor_dump_exps' argument 3 names different: declaration 'exps' definition 'roots'.
boolector-1.5.118-6b56be4-121013/btorexp.c:5526:26: style:inconclusive: Function 'btor_exp_to_aigvec' argument 3 names different: declaration 'table' definition 'backannotation'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btorexp.h:934:24: note: Function 'btor_exp_to_aigvec' argument 3 names different: declaration 'table' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btorexp.c:5526:26: note: Function 'btor_exp_to_aigvec' argument 3 names different: declaration 'table' definition 'backannotation'.
boolector-1.5.118-6b56be4-121013/btorexp.c:346:13: style: Variable 'real_e_if' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:346:25: style: Variable 'real_e_else' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:381:22: style: Parameter 'btor' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1120:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1121:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1190:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1191:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1269:15: style: Variable 'smgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1270:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1348:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1349:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1496:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:1914:13: style: Variable 'real_exp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4131:13: style: Variable 'a' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4132:13: style: Variable 'b' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4388:13: style: Variable 'u' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4715:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4716:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4717:15: style: Variable 'smgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:4881:35: style: Parameter 'btor' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:5434:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:5553:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:6624:19: style: Variable 'real_left' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:6944:22: style: Variable 'bucket' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:6993:28: style: Variable 'real_left' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:6993:40: style: Variable 'real_right' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:8052:24: style: Parameter 'slice' can be declared as pointer to const. However it seems that 'hash_slice' is a callback function, if 'slice' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorexp.c:8142:59: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorexp.c:8052:24: note: Parameter 'slice' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorexp.c:8067:28: style: Parameter 's1' can be declared as pointer to const. However it seems that 'compare_slices' is a callback function, if 's1' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorexp.c:8143:30: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorexp.c:8067:28: note: Parameter 's1' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorexp.c:8067:43: style: Parameter 's2' can be declared as pointer to const. However it seems that 'compare_slices' is a callback function, if 's2' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorexp.c:8143:30: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorexp.c:8067:43: note: Parameter 's2' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorexp.c:8780:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorexp.c:860:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:1597:3: style: Variable 'diffs.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:2438:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:2468:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:4284:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:4627:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:4724:8: style: Variable 'smgr' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:5424:3: style: Variable 'exp_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:5820:3: style: Variable 'queue.head' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:5820:3: style: Variable 'queue.tail' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:5832:3: style: Variable 'unmark_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:6430:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:6441:3: style: Variable 'unmark_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:6660:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:6669:3: style: Variable 'unmark_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7313:7: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7389:7: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7609:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7614:3: style: Variable 'root_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7853:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7953:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:7958:3: style: Variable 'root_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorexp.c:8299:3: style: Variable 'vars.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormem.c:60:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormem.c:73:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormem.c:89:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormem.c:104:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormem.c:81:48: style:inconclusive: Function 'btor_realloc' argument 3 names different: declaration 'oldsz' definition 'old_size'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btormem.h:69:53: note: Function 'btor_realloc' argument 3 names different: declaration 'oldsz' definition 'old_size'.
boolector-1.5.118-6b56be4-121013/btormem.c:81:48: note: Function 'btor_realloc' argument 3 names different: declaration 'oldsz' definition 'old_size'.
boolector-1.5.118-6b56be4-121013/btormem.c:81:65: style:inconclusive: Function 'btor_realloc' argument 4 names different: declaration 'newsz' definition 'new_size'. [funcArgNamesDifferent]
boolector-1.5.118-6b56be4-121013/btormem.h:69:67: note: Function 'btor_realloc' argument 4 names different: declaration 'newsz' definition 'new_size'.
boolector-1.5.118-6b56be4-121013/btormem.c:81:65: note: Function 'btor_realloc' argument 4 names different: declaration 'newsz' definition 'new_size'.
boolector-1.5.118-6b56be4-121013/btorrewrite.c:56:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:80:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:105:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:128:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:239:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:383:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable bits [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1136:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1176:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1345:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1365:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable simplified [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1596:8: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1966:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2025:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2557:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2726:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2887:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3009:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3077:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable len [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3154:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3545:7: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable kind [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btormain.c:853:22: style: Condition 'forced_solvers>=2' is always false [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btormain.c:815:24: note: Assignment 'forced_solvers=0', assigned value is 0
boolector-1.5.118-6b56be4-121013/btormain.c:853:22: note: Condition 'forced_solvers>=2' is always false
boolector-1.5.118-6b56be4-121013/btormain.c:883:7: style: Condition '!used_solvers' is always true [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btormain.c:815:42: note: Assignment 'used_solvers=0', assigned value is 0
boolector-1.5.118-6b56be4-121013/btormain.c:883:7: note: Condition '!used_solvers' is always true
boolector-1.5.118-6b56be4-121013/btormain.c:205:21: style: Redundant assignment of 'delta_time' to itself. [selfAssignment]
boolector-1.5.118-6b56be4-121013/btormain.c:229:3: style: Statements following noreturn function 'raise()' will never be executed. [unreachableCode]
boolector-1.5.118-6b56be4-121013/btormain.c:265:3: style: Statements following noreturn function 'raise()' will never be executed. [unreachableCode]
boolector-1.5.118-6b56be4-121013/btormain.c:276:26: style: Parameter 'app' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btormain.c:287:34: style: Parameter 'app' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btormain.c:410:21: style: Variable 'temp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btormain.c:916:15: style: Variable 'amgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btormain.c:917:18: style: Variable 'avmgr' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btormain.c:915:14: style: Variable 'btor' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:916:20: style: Variable 'amgr' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:917:24: style: Variable 'avmgr' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:918:20: style: Variable 'smgr' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:920:35: style: Variable 'parser_api' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:921:22: style: Variable 'parser' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btormain.c:923:19: style: Variable 'mem' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorsat.c:75:0: error: #error "no usable SAT solver configured" [preprocessorErrorDirective]
boolector-1.5.118-6b56be4-121013/btorsmt.c:412:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:926:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1234:59: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable name [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1257:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1316:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable token [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1419:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable token [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1578:69: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable name [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:2776:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable token [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1730:19: style: Condition 'isarray1' is always true [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorsmt.c:1852:19: style: Condition 'isarray2' is always true [knownConditionTrueFalse]
boolector-1.5.118-6b56be4-121013/btorsmt.c:3072:15: style: Local variable 'next' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/btorsmt.c:2766:21: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/btorsmt.c:3072:15: note: Shadow variable
boolector-1.5.118-6b56be4-121013/btorsmt.c:312:39: style: Parameter 'parser' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorsmt.c:403:35: style: Parameter 'parser' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorsmt.c:674:50: style: Parameter 'opts' can be declared as pointer to const. However it seems that 'btor_new_smt_parser' is a callback function, if 'opts' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorsmt.c:3311:20: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorsmt.c:674:50: note: Parameter 'opts' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorsmt.c:2729:35: style: Parameter 'parser' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorsmt.c:2729:61: style: Parameter 'res' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorsmt.c:3116:19: style: Variable 's' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:211:9: warning: Either the condition 'real_exp' is redundant or there is possible null pointer dereference: real_exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:215:12: note: Assuming that condition 'real_exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorrewrite.c:211:9: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorrewrite.c:222:12: warning: Either the condition 'real_exp' is redundant or there is possible null pointer dereference: real_exp. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:215:12: note: Assuming that condition 'real_exp' is not redundant
boolector-1.5.118-6b56be4-121013/btorrewrite.c:222:12: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1134:7: warning: Either the condition 'real_e0' is redundant or there is possible null pointer dereference: real_e0. [nullPointerRedundantCheck]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1130:7: note: Assuming that condition 'real_e0' is not redundant
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1134:7: note: Null pointer dereference
boolector-1.5.118-6b56be4-121013/btorrewrite.c:73:13: style: Variable 'real_exp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:98:13: style: Variable 'real_exp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:185:14: style: Variable 'real_exp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3128:14: style: Variable 'real_exp' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:675:8: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:910:8: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:1261:3: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2446:11: style: Variable 'real_e0' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2447:11: style: Variable 'real_e1' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2523:13: style: Variable 'real_e0' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:2524:13: style: Variable 'real_e1' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3242:7: style: Variable 'stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorrewrite.c:3243:7: style: Variable 'po_stack.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:641:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:649:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:655:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:668:45: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:874:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:883:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:896:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:911:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:928:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1026:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1304:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1885:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1942:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1985:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:2021:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorutil.c:93:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable RUSAGE_SELF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:83:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:96:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:111:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:150:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:185:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/deltabtor.c:892:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:912:16: warning: Identical inner 'if' condition is always true. [identicalInnerCondition]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:909:15: note: outer condition: open>0
boolector-1.5.118-6b56be4-121013/btorsmt2.c:912:16: note: identical inner condition: open>0
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1765:12: style: Local variable 'len' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1292:27: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1765:12: note: Shadow variable
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1841:6: style: Local variable 'len' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1292:27: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1841:6: note: Shadow variable
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1841:29: style: Local variable 'width' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1292:12: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/btorsmt2.c:1841:29: note: Shadow variable
boolector-1.5.118-6b56be4-121013/btorsmt2.c:570:27: style: Parameter 'opts' can be declared as pointer to const. However it seems that 'btor_new_smt2_parser' is a callback function, if 'opts' is declared with const you might also need to cast function pointer(s). [constParameterCallback]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:2182:20: note: You might need to cast the function pointer here
boolector-1.5.118-6b56be4-121013/btorsmt2.c:570:27: note: Parameter 'opts' can be declared as pointer to const
boolector-1.5.118-6b56be4-121013/btorsmt2.c:632:45: style: Parameter 'parser' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/btorsmt2.c:989:53: style: Parameter 'item' can be declared as pointer to const [constParameterPointer]
boolector-1.5.118-6b56be4-121013/deltabtor.c:216:2: error: Common realloc mistake: 'buf' nulled but not freed upon failure [memleakOnRealloc]
boolector-1.5.118-6b56be4-121013/deltabtor.c:222:5: error: Common realloc mistake: 'buf' nulled but not freed upon failure [memleakOnRealloc]
boolector-1.5.118-6b56be4-121013/deltabtor.c:254:3: error: Common realloc mistake: 'buf' nulled but not freed upon failure [memleakOnRealloc]
boolector-1.5.118-6b56be4-121013/deltabtor.c:261:6: error: Common realloc mistake: 'buf' nulled but not freed upon failure [memleakOnRealloc]
boolector-1.5.118-6b56be4-121013/deltabtor.c:326:6: error: Common realloc mistake: 'exps' nulled but not freed upon failure [memleakOnRealloc]
boolector-1.5.118-6b56be4-121013/deltabtor.c:380:18: style: Local variable 'tmp' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/deltabtor.c:59:15: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/deltabtor.c:380:18: note: Shadow variable
boolector-1.5.118-6b56be4-121013/deltabtor.c:417:18: style: Local variable 'tmp' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/deltabtor.c:59:15: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/deltabtor.c:417:18: note: Shadow variable
boolector-1.5.118-6b56be4-121013/deltabtor.c:874:7: style: Local variable 'tmp' shadows outer variable [shadowVariable]
boolector-1.5.118-6b56be4-121013/deltabtor.c:59:15: note: Shadowed declaration
boolector-1.5.118-6b56be4-121013/deltabtor.c:874:7: note: Shadow variable
boolector-1.5.118-6b56be4-121013/deltabtor.c:381:9: style: Variable 'e' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/deltabtor.c:437:9: style: Variable 'e' can be declared as pointer to const [constVariablePointer]
boolector-1.5.118-6b56be4-121013/synthebtor.c:30:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/synthebtor.c:66:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdin [valueFlowBailoutIncompleteVar]
boolector-1.5.118-6b56be4-121013/synthebtor.c:210:3: style: Variable 'aigs.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/synthebtor.c:214:3: style: Variable 'regs.top' is assigned a value that is never used. [unreadVariable]
boolector-1.5.118-6b56be4-121013/synthebtor.c:218:3: style: Variable 'nexts.top' is assigned a value that is never used. [unreadVariable]
diff:


DONE