2025-05-02 22:57 ftp://ftp.de.debian.org/debian/pool/main/z/z3/z3_4.13.3.orig.tar.gz cppcheck-options: --library=posix --library=gnu --library=bsd --inconclusive --enable=style,information --inline-suppr --template=daca2 --disable=missingInclude --suppress=unmatchedSuppression --check-library --debug-warnings --suppress=autoNoType --suppress=valueFlowBailout --suppress=bailoutUninitVar --suppress=symbolDatabaseWarning --suppress=normalCheckLevelConditionExpressions -D__GNUC__ --platform=unix64 -j1 platform: Linux-6.8.0-59-generic-x86_64-with-glibc2.39 python: 3.12.3 client-version: 1.3.67 compiler: g++ (Ubuntu 14.2.0-4ubuntu2~24.04) 14.2.0 cppcheck: head 2.17.0 head-info: 88ef81e (2025-05-02 08:42:38 +0200) count: 3397 3397 elapsed-time: 30.6 32.6 head-timing-info: old-timing-info: head results: z3-z3-4.13.3/cmake/target_arch_detect.cpp:13:0: error: #error CMAKE_TARGET_ARCH_unknown [preprocessorErrorDirective] z3-z3-4.13.3/cmake/target_arch_detect.cpp:13:2: error: #error CMAKE_TARGET_ARCH_unknown [preprocessorErrorDirective] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:49:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:100:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:130:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:228:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:237:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:259:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:148:24: style: Condition 'delta==0' is always true [knownConditionTrueFalse] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:144:19: note: Assuming that condition 'delta<0' is not redundant z3-z3-4.13.3/contrib/qprofdiff/main.cpp:146:24: note: Assuming that condition 'delta>0' is not redundant z3-z3-4.13.3/contrib/qprofdiff/main.cpp:148:24: note: Condition 'delta==0' is always true z3-z3-4.13.3/contrib/qprofdiff/main.cpp:39:20: performance: Function parameter 'str' should be passed by const reference. [passedByValue] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:96:44: style: Parameter 'data' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:55:24: style: Variable 'cur_token' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:55:14: style: Variable 'cur_token' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:99:10: performance: Prefer prefix ++/-- operators for non-primitive types. [postfixOperator] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:160:9: performance: Prefer prefix ++/-- operators for non-primitive types. [postfixOperator] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:186:9: performance: Prefer prefix ++/-- operators for non-primitive types. [postfixOperator] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:204:9: performance: Prefer prefix ++/-- operators for non-primitive types. [postfixOperator] z3-z3-4.13.3/contrib/qprofdiff/main.cpp:220:9: performance: Prefer prefix ++/-- operators for non-primitive types. [postfixOperator] z3-z3-4.13.3/examples/c++/example.cpp:22:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:46:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:78:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:119:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:157:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:193:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:207:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:225:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:241:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:254:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:276:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:292:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:326:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:345:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:357:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:369:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:398:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:433:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:489:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:533:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:555:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:578:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:611:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:639:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:654:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:688:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:725:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:764:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:785:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:824:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:837:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:851:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:863:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:878:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:901:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:925:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:948:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:961:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1010:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1033:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1056:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1089:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable sat [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1118:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1122:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1131:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1208:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1224:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1242:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1255:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1283:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1287:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1303:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1345:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1361:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c++/example.cpp:1313:55: performance: Function parameter 'value' should be passed by const reference. [passedByValue] z3-z3-4.13.3/examples/c++/example.cpp:1317:49: performance: Function parameter 's' should be passed by const reference. [passedByValue] z3-z3-4.13.3/examples/c++/example.cpp:309:24: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/c++/example.cpp:317:24: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/c++/example.cpp:1415:24: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/c++/example.cpp:1181:9: style: Variable 'instance' can be declared as const array [constVariable] z3-z3-4.13.3/examples/c++/example.cpp:811:16: error: Out of bounds access in expression 'visited[e.id()]' because 'visited' is empty. [containerOutOfBounds] z3-z3-4.13.3/examples/c++/example.cpp:847:11: note: Calling function 'visit', 1st argument 'visited' value is size=0 z3-z3-4.13.3/examples/c++/example.cpp:808:24: note: Assuming condition is false z3-z3-4.13.3/examples/c++/example.cpp:811:16: note: Access out of bounds z3-z3-4.13.3/examples/c/test_capi.c:36:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stderr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:338:45: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_sort [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:436:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_DATATYPE_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:681:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:809:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:849:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1053:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1153:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_UNDEF [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1256:44: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1280:46: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_ARRAY_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1335:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1473:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1506:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1585:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1633:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_OK [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1686:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:1760:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_OK [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2297:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2418:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2472:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2548:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2722:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2875:63: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_func_decl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:2975:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/c/test_capi.c:704:5: warning: %d in format string (no. 1) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:704:5: warning: %d in format string (no. 2) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:704:5: warning: %d in format string (no. 3) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:704:5: warning: %d in format string (no. 4) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:1237:9: warning: %d in format string (no. 1) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:2429:21: warning: %d in format string (no. 1) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/c/test_capi.c:343:32: warning: If memory allocation fails, then there is a possible null pointer dereference: types [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:338:37: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:338:19: note: Assignment 'types=(Z3_sort*)malloc(sizeof(Z3_sort)*sz)', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:343:32: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:344:32: warning: If memory allocation fails, then there is a possible null pointer dereference: names [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:339:39: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:339:19: note: Assignment 'names=(Z3_symbol*)malloc(sizeof(Z3_symbol)*sz)', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:344:32: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:345:32: warning: If memory allocation fails, then there is a possible null pointer dereference: xs [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:340:36: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:340:19: note: Assignment 'xs=(Z3_ast*)malloc(sizeof(Z3_ast)*sz)', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:345:32: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:345:63: warning: If memory allocation fails, then there is a possible null pointer dereference: types [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:338:37: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:338:19: note: Assignment 'types=(Z3_sort*)malloc(sizeof(Z3_sort)*sz)', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:345:63: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:347:11: warning: If memory allocation fails, then there is a possible null pointer dereference: xs [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:340:36: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:340:19: note: Assignment 'xs=(Z3_ast*)malloc(sizeof(Z3_ast)*sz)', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:347:11: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:2337:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ctx [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:2336:57: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:2336:34: note: Assignment 'ctx=(struct Z3_ext_context_struct*)malloc(sizeof(struct Z3_ext_context_struct))', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:2337:5: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:2338:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ctx [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:2336:57: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:2336:34: note: Assignment 'ctx=(struct Z3_ext_context_struct*)malloc(sizeof(struct Z3_ext_context_struct))', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:2338:5: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:2338:44: warning: If memory allocation fails, then there is a possible null pointer dereference: ctx [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:2336:57: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:2336:34: note: Assignment 'ctx=(struct Z3_ext_context_struct*)malloc(sizeof(struct Z3_ext_context_struct))', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:2338:44: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:2339:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ctx [nullPointerOutOfMemory] z3-z3-4.13.3/examples/c/test_capi.c:2336:57: note: Assuming allocation function fails z3-z3-4.13.3/examples/c/test_capi.c:2336:34: note: Assignment 'ctx=(struct Z3_ext_context_struct*)malloc(sizeof(struct Z3_ext_context_struct))', assigned value is 0 z3-z3-4.13.3/examples/c/test_capi.c:2339:5: note: Null pointer dereference z3-z3-4.13.3/examples/c/test_capi.c:2003:8: style: Variable 'l2' is reassigned a value before the old one has been used. [redundantAssignment] z3-z3-4.13.3/examples/c/test_capi.c:1992:8: note: l2 is assigned z3-z3-4.13.3/examples/c/test_capi.c:2003:8: note: l2 is overwritten z3-z3-4.13.3/examples/c/test_capi.c:1246:23: style: Local variable 's' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/c/test_capi.c:1227:15: note: Shadowed declaration z3-z3-4.13.3/examples/c/test_capi.c:1246:23: note: Shadow variable z3-z3-4.13.3/examples/maxsat/maxsat.c:25:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stderr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:75:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_ast [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:227:41: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_ast [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:349:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_TRUE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:414:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:469:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_ast [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:541:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_L_FALSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:592:44: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_ast [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/maxsat/maxsat.c:427:9: warning: %d in format string (no. 1) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/maxsat/maxsat.c:554:9: warning: %d in format string (no. 1) requires 'int' but the argument type is 'unsigned int'. [invalidPrintfArgType_sint] z3-z3-4.13.3/examples/maxsat/maxsat.c:78:9: warning: If memory allocation fails, then there is a possible null pointer dereference: result [nullPointerOutOfMemory] z3-z3-4.13.3/examples/maxsat/maxsat.c:75:40: note: Assuming allocation function fails z3-z3-4.13.3/examples/maxsat/maxsat.c:75:23: note: Assignment 'result=(Z3_ast*)malloc(sizeof(Z3_ast)*num_vars)', assigned value is 0 z3-z3-4.13.3/examples/maxsat/maxsat.c:78:9: note: Null pointer dereference z3-z3-4.13.3/examples/maxsat/maxsat.c:229:12: warning: If memory allocation fails, then there is a possible null pointer dereference: aux_1 [nullPointerOutOfMemory] z3-z3-4.13.3/examples/maxsat/maxsat.c:227:33: note: Assuming allocation function fails z3-z3-4.13.3/examples/maxsat/maxsat.c:227:16: note: Assignment 'aux_1=(Z3_ast*)malloc(sizeof(Z3_ast)*(n+1))', assigned value is 0 z3-z3-4.13.3/examples/maxsat/maxsat.c:229:12: note: Null pointer dereference z3-z3-4.13.3/examples/maxsat/maxsat.c:479:9: warning: If memory allocation fails, then there is a possible null pointer dereference: assumptions [nullPointerOutOfMemory] z3-z3-4.13.3/examples/maxsat/maxsat.c:469:44: note: Assuming allocation function fails z3-z3-4.13.3/examples/maxsat/maxsat.c:469:28: note: Assignment 'assumptions=(Z3_ast*)malloc(sizeof(Z3_ast)*num_soft_cnstrs)', assigned value is 0 z3-z3-4.13.3/examples/maxsat/maxsat.c:479:9: note: Null pointer dereference z3-z3-4.13.3/examples/maxsat/maxsat.c:594:9: warning: If memory allocation fails, then there is a possible null pointer dereference: hard_cnstrs [nullPointerOutOfMemory] z3-z3-4.13.3/examples/maxsat/maxsat.c:592:36: note: Assuming allocation function fails z3-z3-4.13.3/examples/maxsat/maxsat.c:592:19: note: Assignment 'hard_cnstrs=(Z3_ast*)malloc(sizeof(Z3_ast)*(num_hard_cnstrs))', assigned value is 0 z3-z3-4.13.3/examples/maxsat/maxsat.c:594:9: note: Null pointer dereference z3-z3-4.13.3/examples/maxsat/maxsat.c:605:9: warning: If memory allocation fails, then there is a possible null pointer dereference: soft_cnstrs [nullPointerOutOfMemory] z3-z3-4.13.3/examples/maxsat/maxsat.c:603:36: note: Assuming allocation function fails z3-z3-4.13.3/examples/maxsat/maxsat.c:603:19: note: Assignment 'soft_cnstrs=(Z3_ast*)malloc(sizeof(Z3_ast)*(num_soft_cnstrs))', assigned value is 0 z3-z3-4.13.3/examples/maxsat/maxsat.c:605:9: note: Null pointer dereference z3-z3-4.13.3/examples/maxsat/maxsat.c:23:19: style: Parameter 'msg' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/maxsat/maxsat.c:144:93: style: Parameter 'cnstrs' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/maxsat/maxsat.c:219:66: style: Parameter 'lits' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/maxsat/maxsat.c:182:24: warning: Uninitialized variable: cout [uninitvar] z3-z3-4.13.3/examples/maxsat/maxsat.c:177:19: note: Assuming condition is false z3-z3-4.13.3/examples/maxsat/maxsat.c:182:24: note: Uninitialized variable: cout z3-z3-4.13.3/examples/maxsat/maxsat.c:474:16: style: Variable 'k' is assigned a value that is never used. [unreadVariable] tptp5.y:43:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stderr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1490:41: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_OP_PR_LEMMA [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1731:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1913:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_UNINTERPRETED_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1926:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_OP_UNINTERPRETED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1957:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_INT_SYMBOL [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2005:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2027:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2038:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable SIG_DFL [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2158:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2212:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_OP_AND [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2224:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2288:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2304:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cerr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2368:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cerr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2487:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cerr [valueFlowBailoutIncompleteVar] tptp5.tab.c:1995:5: warning: Assignment of function parameter has no effect outside the function. Did you forget dereferencing it? [uselessAssignmentPtrArg] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1197:5: warning: Member variable 'pp_tptp::m_node_number' is not initialized in the constructor. [uninitMemberVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1197:5: warning: Member variable 'pp_tptp::m_named_formulas' is not initialized in the constructor. [uninitMemberVar] z3-z3-4.13.3/examples/tptp/tptp5.cpp:937:10: style: Unused private function: 'env::check_app' [unusedPrivateFunction] z3-z3-4.13.3/examples/tptp/tptp5.cpp:937:10: note: Unused private function: 'env::check_app' z3-z3-4.13.3/examples/tptp/tptp5.cpp:937:10: note: Unused private function: 'env::check_app' z3-z3-4.13.3/examples/tptp/tptp5.cpp:192:10: performance:inconclusive: Technically the member function 'env::mk_error' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:199:10: performance:inconclusive: Technically the member function 'env::mk_not_handled' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:235:10: performance:inconclusive: Technically the member function 'env::check_arity' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:537:10: performance:inconclusive: Technically the member function 'env::is_ttype' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:914:14: performance:inconclusive: Technically the member function 'env::to_int' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:918:14: performance:inconclusive: Technically the member function 'env::to_real' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:926:14: performance:inconclusive: Technically the member function 'env::is_even' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:937:10: performance:inconclusive: Technically the member function 'env::check_app' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1004:10: performance:inconclusive: Technically the member function 'env::is_sep' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1380:10: performance:inconclusive: Technically the member function 'pp_tptp::display_sort' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1865:10: performance:inconclusive: Technically the member function 'pp_tptp::display_sort_decl' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1955:17: performance:inconclusive: Technically the member function 'pp_tptp::sanitize' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/examples/tptp/tptp5.cpp:139:9: warning: Class 'TreeNode' does not have a copy constructor which is recommended since it has dynamic memory/resource allocation(s). [noCopyConstructor] z3-z3-4.13.3/examples/tptp/tptp5.cpp:139:9: warning: Class 'TreeNode' does not have a operator= which is recommended since it has dynamic memory/resource allocation(s). [noOperatorEq] z3-z3-4.13.3/examples/tptp/tptp5.cpp:139:9: warning: Class 'TreeNode' does not have a destructor which is recommended since it has dynamic memory/resource allocation(s). [noDestructor] z3-z3-4.13.3/examples/tptp/tptp5.cpp:114:5: style: Struct 'failure_ex' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1114:5: style: Class 'env' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1197:5: style: Class 'pp_tptp' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1011:16: style: Condition 'sz>0' is always true [knownConditionTrueFalse] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1010:16: note: Assuming that condition 'sz==0' is not redundant z3-z3-4.13.3/examples/tptp/tptp5.cpp:1011:16: note: Condition 'sz>0' is always true tptp5.y:52:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:52:5: note: Null pointer dereference tptp5.y:53:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:53:5: note: Null pointer dereference tptp5.y:54:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:54:5: note: Null pointer dereference tptp5.y:55:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:55:5: note: Null pointer dereference tptp5.y:56:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:56:5: note: Null pointer dereference tptp5.y:57:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:57:5: note: Null pointer dereference tptp5.y:58:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:58:5: note: Null pointer dereference tptp5.y:59:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:59:5: note: Null pointer dereference tptp5.y:60:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:60:5: note: Null pointer dereference tptp5.y:61:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:61:5: note: Null pointer dereference tptp5.y:62:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:62:5: note: Null pointer dereference tptp5.y:63:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:63:5: note: Null pointer dereference tptp5.y:64:5: warning: If memory allocation fails, then there is a possible null pointer dereference: ss [nullPointerOutOfMemory] tptp5.y:50:29: note: Assuming allocation function fails tptp5.y:50:16: note: Assignment 'ss=(struct pTreeNodepTree)calloc(1,sizeof(struct pTreeNode))', assigned value is 0 tptp5.y:64:5: note: Null pointer dereference tptp5.y:50:17: style: C-style pointer casting [cstyleCast] tptp5.tab.c:2178:5: style: C-style pointer casting [cstyleCast] tptp5.y:253:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:260:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:267:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:274:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:281:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:288:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:295:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:302:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:309:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:316:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:323:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:330:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:337:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:344:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:351:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:358:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:365:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:372:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:379:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:386:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:393:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:400:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:407:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:414:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:421:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:428:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:435:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:442:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:449:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:456:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:463:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:470:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:477:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:484:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:491:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:498:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:505:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:512:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:519:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:526:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:533:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:540:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:547:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:554:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:561:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:568:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:575:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:582:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:589:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:596:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:603:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:610:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:617:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:624:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:631:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:638:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:645:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:652:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:659:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:666:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:673:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:680:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:687:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:694:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:701:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:708:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:715:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:722:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:729:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:736:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:743:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:750:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:757:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:764:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:771:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:778:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:785:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:792:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:799:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:806:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:813:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:820:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:827:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:834:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:841:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:848:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:855:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:862:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:869:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:876:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:883:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:890:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:897:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:904:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:911:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:918:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:925:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:932:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:939:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:946:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:953:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:960:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:967:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:974:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:981:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:988:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:995:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1002:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1009:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1016:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1023:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1030:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1037:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1044:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1051:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1058:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1065:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1072:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1079:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1086:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1093:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1100:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1107:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1114:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1121:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1128:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1135:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1142:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1149:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1156:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1163:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1170:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1177:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1184:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1191:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1198:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1205:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1212:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1219:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1226:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1233:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1240:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1247:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1254:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1261:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1268:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1275:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1282:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1289:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1296:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1303:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1310:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1317:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1324:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1331:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1338:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1345:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1352:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1359:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1366:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1373:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1380:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1387:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1394:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1401:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1408:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1415:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1422:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1429:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1436:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1443:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1450:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1457:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1464:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1471:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1478:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1485:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1492:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1499:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1506:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1513:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1520:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1527:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1534:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1541:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1548:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1555:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1562:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1569:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1576:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1583:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1590:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1597:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1604:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1611:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1618:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1625:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1632:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1639:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1646:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1653:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1660:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1667:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1674:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1681:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1688:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1695:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1702:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1709:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1716:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1723:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1730:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1737:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1744:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1751:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1758:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1765:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1772:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1779:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1786:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1793:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1800:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1807:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1814:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1821:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1828:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1835:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1842:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1849:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1856:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1863:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1870:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1877:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1884:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1891:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1898:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1905:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1912:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1919:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1926:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1933:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1940:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1947:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1954:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1961:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1968:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1975:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1982:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1989:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:1996:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2003:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2010:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2017:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2024:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2031:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2038:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2045:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2052:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2059:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2066:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2073:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2080:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2087:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2094:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2101:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2108:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2115:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2122:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2129:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2136:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2143:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2150:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2157:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2164:21: style: Same expression on both sides of '-'. [duplicateExpression] tptp5.y:2171:21: style: Same expression on both sides of '-'. [duplicateExpression] z3-z3-4.13.3/examples/tptp/tptp5.cpp:266:13: style:inconclusive: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/examples/tptp/tptp5.cpp:718:24: style: Local variable 's' shadows outer argument [shadowArgument] z3-z3-4.13.3/examples/tptp/tptp5.cpp:667:44: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:718:24: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1555:26: style: Local variable 'id' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1517:22: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1555:26: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1718:26: style: Local variable 'conclusion' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1698:18: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1718:26: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1791:22: style: Local variable 'e' shadows outer argument [shadowArgument] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1786:40: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1791:22: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1806:26: style: Local variable 'sz' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1788:16: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1806:26: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1833:18: style: Local variable 'sorts' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1185:32: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1833:18: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1834:20: style: Local variable 'names' shadows outer variable [shadowVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1184:32: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1834:20: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:1883:22: style: Local variable 'e' shadows outer argument [shadowArgument] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1880:33: note: Shadowed declaration z3-z3-4.13.3/examples/tptp/tptp5.cpp:1883:22: note: Shadow variable z3-z3-4.13.3/examples/tptp/tptp5.cpp:121:35: style: Parameter 'r' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:988:60: style: Parameter 'fml' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:1865:57: style: Parameter 's' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2303:24: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2367:24: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:2412:32: style: Variable 'ex' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/examples/tptp/tptp5.cpp:163:11: style: Variable 'symbol' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:192:29: style: Parameter 'f' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:199:35: style: Parameter 'f' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:241:31: style: Parameter 'file_name' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:241:52: style: Parameter 'formula_selection' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:296:50: style: Parameter 'formula_role' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:320:32: style: Parameter 'formula' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:339:32: style: Parameter 'd' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:352:28: style: Parameter 'l' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:362:74: style: Parameter 'formula' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:537:29: style: Parameter 't' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:545:43: style: Parameter 'fol_quantifier' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:558:37: style: Parameter 'variable_list' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:626:23: style: Variable 't1' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/examples/tptp/tptp5.cpp:951:28: style: Parameter 'args' can be declared as pointer to const [constParameterPointer] tptp5.y:88:10: style: Variable 'c1' can be declared as const array [constVariable] tptp5.y:88:23: style: Variable 'c2' can be declared as const array [constVariable] z3-z3-4.13.3/examples/tptp/tptp5.cpp:335:15: style: Consider using std::any_of, std::all_of, std::none_of, or std::accumulate algorithm instead of a raw loop. [useStlAlgorithm] tptp5.tab.c:1995:11: style: Variable 'yymsg' is assigned a value that is never used. [unreadVariable] tptp5.lex.cpp:920:11: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stdin [valueFlowBailoutIncompleteVar] tptp5.lex.cpp:1873:3: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar] tptp5.lex.cpp:2056:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable EOF [valueFlowBailoutIncompleteVar] tptp5.lex.cpp:2208:15: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable errno [valueFlowBailoutIncompleteVar] tptp5.lex.cpp:2450:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable stderr [valueFlowBailoutIncompleteVar] tptp5.lex.cpp:1750:16: style: Condition 'yywrap()' is always true [knownConditionTrueFalse] tptp5.lex.cpp:1750:16: note: Calling function 'yywrap' returns 1 tptp5.lex.cpp:1750:16: note: Condition 'yywrap()' is always true tptp5.lex.cpp:2055:17: style: Condition 'yywrap()' is always true [knownConditionTrueFalse] tptp5.lex.cpp:2055:17: note: Calling function 'yywrap' returns 1 tptp5.lex.cpp:2055:17: note: Condition 'yywrap()' is always true tptp5.lex.cpp:2162:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2159:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2162:2: note: Null pointer dereference tptp5.lex.cpp:2167:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2159:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2167:2: note: Null pointer dereference tptp5.lex.cpp:2167:34: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2159:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2167:34: note: Null pointer dereference tptp5.lex.cpp:2168:9: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2159:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2168:9: note: Null pointer dereference tptp5.lex.cpp:2212:2: warning: Possible null pointer dereference: b [nullPointer] tptp5.lex.cpp:2101:17: note: Calling function 'yy_init_buffer', 1st argument '(yy_buffer_stack)?(yy_buffer_stack)[yy_buffer_stack_top]:NULL' value is 0 tptp5.lex.cpp:2212:2: note: Null pointer dereference tptp5.lex.cpp:2213:2: warning: Possible null pointer dereference: b [nullPointer] tptp5.lex.cpp:2101:17: note: Calling function 'yy_init_buffer', 1st argument '(yy_buffer_stack)?(yy_buffer_stack)[yy_buffer_stack_top]:NULL' value is 0 tptp5.lex.cpp:2213:2: note: Null pointer dereference tptp5.lex.cpp:2378:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2378:2: note: Null pointer dereference tptp5.lex.cpp:2379:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2379:2: note: Null pointer dereference tptp5.lex.cpp:2379:18: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2379:18: note: Null pointer dereference tptp5.lex.cpp:2380:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2380:2: note: Null pointer dereference tptp5.lex.cpp:2381:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2381:2: note: Null pointer dereference tptp5.lex.cpp:2382:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2382:2: note: Null pointer dereference tptp5.lex.cpp:2382:23: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2382:23: note: Null pointer dereference tptp5.lex.cpp:2383:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2383:2: note: Null pointer dereference tptp5.lex.cpp:2384:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2384:2: note: Null pointer dereference tptp5.lex.cpp:2385:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2385:2: note: Null pointer dereference tptp5.lex.cpp:2386:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2375:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2386:2: note: Null pointer dereference tptp5.lex.cpp:2439:2: warning: Either the condition '!b' is redundant or there is possible null pointer dereference: b. [nullPointerRedundantCheck] tptp5.lex.cpp:2433:7: note: Assuming that condition '!b' is not redundant tptp5.lex.cpp:2439:2: note: Null pointer dereference tptp5.lex.cpp:912:30: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:1901:41: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:1901:60: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2074:7: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2158:7: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2167:17: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2192:10: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2194:9: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2326:24: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2345:24: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2374:7: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2423:8: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2650:27: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:2655:8: style: C-style pointer casting [cstyleCast] tptp5.lex.cpp:1873:3: style: Redundant initialization for 'c'. The initialized value is overwritten before it is read. [redundantInitialization] tptp5.lex.cpp:1873:3: note: c is initialized tptp5.lex.cpp:1873:3: note: c is overwritten tptp5.l:117:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:126:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:135:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:144:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:153:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:162:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:171:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:180:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:189:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:198:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:207:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:216:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:225:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:234:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:243:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:252:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:261:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:270:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:279:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:288:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:297:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:307:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:316:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:325:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:334:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:343:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:352:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:361:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:370:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:379:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:388:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:397:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:406:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:415:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:424:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:433:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:442:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:451:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:460:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:469:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:479:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:489:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:499:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:509:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:519:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:528:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:537:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:546:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:555:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:564:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:573:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:582:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:591:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:600:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:609:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:618:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:627:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:636:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:645:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:654:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:663:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:672:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:681:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:690:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:699:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:708:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:717:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:726:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:735:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.l:744:2: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] tptp5.lex.cpp:1861:23: style: Checking if unsigned expression 'num_to_read' is less than zero. [unsignedLessThanZero] tptp5.lex.cpp:1948:59: style:inconclusive: Function 'yy_try_NUL_trans' argument 1 names different: declaration 'current_state' definition 'yy_current_state'. [funcArgNamesDifferent] tptp5.lex.cpp:362:54: note: Function 'yy_try_NUL_trans' argument 1 names different: declaration 'current_state' definition 'yy_current_state'. tptp5.lex.cpp:1948:59: note: Function 'yy_try_NUL_trans' argument 1 names different: declaration 'current_state' definition 'yy_current_state'. tptp5.lex.cpp:1967:41: style:inconclusive: Function 'yyunput' argument 2 names different: declaration 'buf_ptr' definition 'yy_bp'. [funcArgNamesDifferent] tptp5.lex.cpp:774:38: note: Function 'yyunput' argument 2 names different: declaration 'buf_ptr' definition 'yy_bp'. tptp5.lex.cpp:1967:41: note: Function 'yyunput' argument 2 names different: declaration 'buf_ptr' definition 'yy_bp'. tptp5.lex.cpp:2401:48: style:inconclusive: Function 'yy_scan_string' argument 1 names different: declaration 'yy_str' definition 'yystr'. [funcArgNamesDifferent] tptp5.lex.cpp:315:47: note: Function 'yy_scan_string' argument 1 names different: declaration 'yy_str' definition 'yystr'. tptp5.lex.cpp:2401:48: note: Function 'yy_scan_string' argument 1 names different: declaration 'yy_str' definition 'yystr'. tptp5.lex.cpp:2414:48: style:inconclusive: Function 'yy_scan_bytes' argument 1 names different: declaration 'bytes' definition 'yybytes'. [funcArgNamesDifferent] tptp5.lex.cpp:316:46: note: Function 'yy_scan_bytes' argument 1 names different: declaration 'bytes' definition 'yybytes'. tptp5.lex.cpp:2414:48: note: Function 'yy_scan_bytes' argument 1 names different: declaration 'bytes' definition 'yybytes'. tptp5.lex.cpp:2414:62: style:inconclusive: Function 'yy_scan_bytes' argument 2 names different: declaration 'len' definition '_yybytes_len'. [funcArgNamesDifferent] tptp5.lex.cpp:316:56: note: Function 'yy_scan_bytes' argument 2 names different: declaration 'len' definition '_yybytes_len'. tptp5.lex.cpp:2414:62: note: Function 'yy_scan_bytes' argument 2 names different: declaration 'len' definition '_yybytes_len'. tptp5.lex.cpp:2546:24: style:inconclusive: Function 'yyset_debug' argument 1 names different: declaration 'debug_flag' definition 'bdebug'. [funcArgNamesDifferent] tptp5.lex.cpp:740:23: note: Function 'yyset_debug' argument 1 names different: declaration 'debug_flag' definition 'bdebug'. tptp5.lex.cpp:2546:24: note: Function 'yyset_debug' argument 1 names different: declaration 'debug_flag' definition 'bdebug'. tptp5.lex.cpp:1815:9: style: Variable 'source' can be declared as pointer to const [constVariablePointer] tptp5.lex.cpp:1982:10: style: Variable 'source' can be declared as pointer to const [constVariablePointer] tptp5.l:45:27: style: Parameter 'lval' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/examples/userPropagator/user_propagator_subquery_maximisation.h:36:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable unsat [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/userPropagator/example.cpp:75:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable sat [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/userPropagator/example.cpp:282:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/examples/userPropagator/user_propagator.h:11:18: style:inconclusive: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. [initializerList] z3-z3-4.13.3/examples/userPropagator/user_propagator.h:53:90: note: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. z3-z3-4.13.3/examples/userPropagator/user_propagator.h:11:18: note: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. z3-z3-4.13.3/examples/userPropagator/user_propagator.h:11:18: style:inconclusive: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. [initializerList] z3-z3-4.13.3/examples/userPropagator/user_propagator.h:60:98: note: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. z3-z3-4.13.3/examples/userPropagator/user_propagator.h:11:18: note: Member variable 'user_propagator::currentModel' is in the wrong place in the initializer list. z3-z3-4.13.3/examples/userPropagator/user_propagator_subquery_maximisation.h:41:13: style: The scope of the variable 'prev' can be reduced. [variableScope] z3-z3-4.13.3/examples/userPropagator/example.cpp:173:9: style: The scope of the variable 'prev' can be reduced. [variableScope] z3-z3-4.13.3/examples/userPropagator/example.cpp:206:9: style: The scope of the variable 'prev' can be reduced. [variableScope] z3-z3-4.13.3/examples/userPropagator/example.cpp:266:9: style: The scope of the variable 'prev' can be reduced. [variableScope] z3-z3-4.13.3/examples/userPropagator/common.h:31:11: style: Checking if unsigned expression 'n' is less than zero. [unsignedLessThanZero] z3-z3-4.13.3/examples/userPropagator/user_propagator_with_theory.h:26:30: style: Local variable 'fixed' shadows outer function [shadowFunction] z3-z3-4.13.3/examples/userPropagator/user_propagator_with_theory.h:15:10: note: Shadowed declaration z3-z3-4.13.3/examples/userPropagator/user_propagator_with_theory.h:26:30: note: Shadow variable z3-z3-4.13.3/examples/userPropagator/user_propagator_created_maximisation.h:173:40: style: Consider using std::copy_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/examples/userPropagator/example.cpp:47:18: style: Consider using std::copy algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/examples/userPropagator/example.cpp:124:30: style: Variable 'idMapping[queens[i]]' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/examples/userPropagator/example.cpp:198:30: style: Variable 'idMapping[queens[i]]' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/examples/userPropagator/example.cpp:230:30: style: Variable 'idMapping[queens[i]]' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/src/ackermannization/ackermannize_bv_tactic.cpp:38:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ackermannization/ackr_bound_probe.cpp:72:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ackermannization/ackr_model_converter.cpp:46:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ackermannization/lackr.cpp:68:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ackermannization/lackr_model_constructor.cpp:202:13: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ackermannization/lackr_model_converter_lazy.cpp:34:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable model [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_algebraic.cpp:346:9: style: Class 'vector_var2anum' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/api/api_algebraic.cpp:87:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_algebraic.cpp:296:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_algebraic.cpp:318:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_algebraic.cpp:448:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_algebraic.cpp:433:26: style: Local variable 'c' shadows outer argument [shadowArgument] z3-z3-4.13.3/src/api/api_algebraic.cpp:420:59: note: Shadowed declaration z3-z3-4.13.3/src/api/api_algebraic.cpp:433:26: note: Shadow variable z3-z3-4.13.3/src/api/api_algebraic.cpp:346:46: style: Parameter 'as' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/src/api/api_arith.cpp:90:15: style: Variable 'ty' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/api/api_arith.cpp:91:15: style: Variable 'real_ty' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/api/api_array.cpp:244:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_array.cpp:282:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:60:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:74:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:347:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:356:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:369:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:509:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:527:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:545:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:563:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:635:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:645:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:664:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:673:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:771:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:801:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:823:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:1031:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:1066:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:1425:17: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] z3-z3-4.13.3/src/api/api_ast.cpp:1455:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast.cpp:1473:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast_map.cpp:64:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast_map.cpp:132:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast_map.cpp:165:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast_vector.cpp:59:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_ast_vector.cpp:135:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:176:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:254:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:287:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:344:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:370:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_bv.cpp:399:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_context.cpp:169:13: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/api/api_datalog.cpp:254:24: error: syntax error [syntaxError] z3-z3-4.13.3/src/api/api_datatype.cpp:217:9: style: Struct 'constructor' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/api/api_datatype.cpp:255:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_datatype.cpp:459:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_datatype.cpp:578:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_datatype.cpp:253:22: style: Local variable 'c' shadows outer argument [shadowArgument] z3-z3-4.13.3/src/api/api_datatype.cpp:244:58: note: Shadowed declaration z3-z3-4.13.3/src/api/api_datatype.cpp:253:22: note: Shadow variable z3-z3-4.13.3/src/api/api_fpa.cpp:912:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:938:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:971:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:1004:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:1043:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:1075:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:1120:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:1160:36: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/api/api_fpa.cpp:882:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:896:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:926:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1026:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1063:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1104:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1148:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1238:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1252:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1266:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1280:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1294:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1308:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_fpa.cpp:1322:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_goal.cpp:79:24: error: syntax error [syntaxError] z3-z3-4.13.3/src/api/api_log.cpp:76:50: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:77:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:78:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:79:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:80:56: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:81:79: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:93:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:95:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:96:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:97:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:98:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:99:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:100:102: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable endl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/api_log.cpp:37:18: style: Parameter 'obj' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/api/api_log.cpp:41:18: style: Parameter 'obj' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/api/api_log.cpp:45:19: style: Parameter 'obj' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/api/api_log.cpp:77:15: style: Parameter 'obj' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/api/api_model.cpp:171:30: error: Internal error. VarId set for bool literal. [internalError] z3-z3-4.13.3/src/api/api_numeral.cpp:155:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:177:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:339:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:359:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:378:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:399:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:419:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_numeral.cpp:445:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_opt.cpp:78:24: error: syntax error [syntaxError] z3-z3-4.13.3/src/api/api_params.cpp:120:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_params.cpp:169:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_params.cpp:182:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_params.cpp:195:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_params.cpp:212:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_parsers.cpp:42:9: style: Struct 'Z3_parser_context_ref' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/api/api_parsers.cpp:158:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_parsers.cpp:196:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_qe.cpp:67:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_qe.cpp:104:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_qe.cpp:127:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_qe.cpp:164:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_qe.cpp:158:23: style: Consider using std::copy algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/api/api_quant.cpp:104:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_quant.cpp:351:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_quant.cpp:359:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_quant.cpp:367:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:222:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:231:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:240:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:249:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:258:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:267:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:278:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:289:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:311:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:320:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:329:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:338:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:347:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:356:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:365:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:375:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:385:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:398:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:408:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:418:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:428:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_rcf.cpp:438:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:117:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:125:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:159:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:168:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:176:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:189:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:236:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_seq.cpp:248:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_solver.cpp:530:24: error: syntax error [syntaxError] z3-z3-4.13.3/src/api/api_stats.cpp:36:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:61:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:73:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:85:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:97:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:113:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_stats.cpp:129:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:331:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:343:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:351:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:363:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:375:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:400:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:413:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:450:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:504:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:512:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:570:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:582:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:638:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/api_tactic.cpp:667:9: style: Statements following 'return' will never be executed. [unreachableCode] z3-z3-4.13.3/src/api/julia/z3jl.cpp:118:17: debug: Failed to parse 'typedef typename decltype ( wrapped ) :: type WrappedT ;'. The checking continues anyway. [simplifyTypedef] z3-z3-4.13.3/src/api/julia/z3jl.cpp:325:70: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:326:89: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:327:82: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:328:73: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:329:96: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:330:87: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:331:87: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:332:110: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:333:124: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:334:138: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:523:26: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:543:25: debug: simplifyOperatorName: found unsimplified operator name [debug] z3-z3-4.13.3/src/api/julia/z3jl.cpp:63:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable RNA [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/api/julia/z3jl.cpp:193:57: style: C-style reference casting [cstyleCast] z3-z3-4.13.3/src/api/julia/z3jl.cpp:195:57: style: C-style reference casting [cstyleCast] z3-z3-4.13.3/src/api/julia/z3jl.cpp:257:0: style: C-style reference casting [cstyleCast] z3-z3-4.13.3/src/api/julia/z3jl.cpp:326:0: style: C-style reference casting [cstyleCast] z3-z3-4.13.3/src/api/julia/z3jl.cpp:327:0: style: C-style reference casting [cstyleCast] z3-z3-4.13.3/src/api/z3_replayer.cpp:33:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/act_cache.cpp:160:9: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/arith_decl_plugin.cpp:42:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/array_decl_plugin.cpp:68:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/array_peq.cpp:40:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eq [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/array_peq.cpp:60:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_peq [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/array_peq.cpp:87:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_decl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/array_peq.cpp:97:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_lhs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.cpp:3064:5: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/ast_ll_pp.cpp:162:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_ll_pp.cpp:256:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable forall_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_ll_pp.cpp:155:10: style:inconclusive: Technically the member function 'll_printer::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/ast_ll_pp.cpp:155:27: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast_pp_dot.cpp:84:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:39:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:79:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:95:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:110:47: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:124:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:151:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_defined_lim [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:160:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_pp_util.cpp:188:88: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_printer.cpp:28:78: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable smt2_pp_environment_dbg [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_printer.cpp:55:68: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_printer.cpp:56:71: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable cerr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_printer.cpp:28:64: performance: Variable 'm_env' is assigned in constructor body. Consider performing initialization in initialization list. [useInitializationList] z3-z3-4.13.3/src/ast/ast_printer.cpp:28:5: style: Class 'simple_ast_printer_context' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast_smt2_pp.cpp:705:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:139:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:198:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BOOL_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:208:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable PROOF_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:236:45: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_UMINUS [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:307:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BV_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:522:67: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:854:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable DATATYPE_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:918:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:925:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:941:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:949:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:718:5: warning: Member variable 'smt_printer::m_top' is not initialized in the constructor. [uninitMemberVar] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:301:10: style: Unused private function: 'smt_printer::is_auflira' [unusedPrivateFunction] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:301:10: note: Unused private function: 'smt_printer::is_auflira' z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:301:10: note: Unused private function: 'smt_printer::is_auflira' z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:738:9: performance: Variable 'm_basic_fid' is assigned in constructor body. Consider performing initialization in initialization list. [useInitializationList] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:195:10: style:inconclusive: Technically the member function 'smt_printer::is_bool' can be const. [functionConst] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:205:10: style:inconclusive: Technically the member function 'smt_printer::is_proof' can be const. [functionConst] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:245:10: performance:inconclusive: Technically the member function 'smt_printer::is_sort_param' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:674:31: style: The if condition is the same as the previous if condition [duplicateCondition] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:671:31: note: First condition z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:674:31: note: Second condition z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:455:26: style: Local variable 's' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:364:17: note: Shadowed declaration z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:455:26: note: Shadow variable z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:821:28: style: Local variable 's' shadows outer argument [shadowArgument] z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:788:38: note: Shadowed declaration z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:821:28: note: Shadow variable z3-z3-4.13.3/src/ast/ast_smt_pp.cpp:455:26: style: Variable 's' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/ast/ast_translation.cpp:199:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/ast_util.cpp:171:40: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/ast_util.cpp:184:39: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/ast_util.cpp:276:18: style: Variable 'a' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/ast/ast_util.cpp:346:18: style: Variable 'a' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/ast/ast_util.cpp:135:0: style: Consider using std::any_of algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/ast_util.cpp:278:24: style: Consider using std::copy algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/ast_util.cpp:348:24: style: Consider using std::copy algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/bv_decl_plugin.cpp:694:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:29:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_char [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:34:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:116:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_char [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:121:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_CHAR_LE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:130:50: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable CHAR_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/char_decl_plugin.cpp:164:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/equiv_proof_converter.cpp:31:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:38:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:142:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:171:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:194:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:216:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:281:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:303:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:370:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:393:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:409:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:427:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:475:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:483:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:567:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:623:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:656:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:688:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:765:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:797:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_inverters [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:816:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:821:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:831:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:862:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:880:10: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:892:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_inverters [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:898:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mc [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:905:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_produce_proofs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:151:5: style: Class 'arith_expr_inverter' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:493:9: style: Class 'bv_expr_inverter' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:677:5: style: Class 'dt_expr_inverter' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:750:5: style: Class 'seq_expr_inverter' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:435:19: style: The scope of the variable 'v' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/converters/expr_inverter.cpp:453:19: style: The scope of the variable 'v' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/converters/generic_model_converter.cpp:39:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/converters/horn_subsume_model_converter.cpp:111:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:35:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:43:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:53:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:63:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable model [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:88:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_c1 [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:175:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_env [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:198:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable model [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:142:5: style: Class 'model2mc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/converters/model_converter.cpp:203:34: style: Parameter 'mc' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/src/ast/converters/replace_proof_converter.cpp:69:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/cost_evaluator.cpp:86:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_args [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/cost_evaluator.cpp:94:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_args [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/datatype_decl_plugin.cpp:861:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/decl_collector.cpp:29:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_dt_fid [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:56:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rec_fid [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:73:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:82:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_basic_fid [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:91:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:152:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable sort_set [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:161:50: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable DATATYPE_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:197:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_trail_lim [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/decl_collector.cpp:50:16: style: The scope of the variable 'g' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/decl_collector.cpp:172:31: style: Local variable 'i' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/decl_collector.cpp:166:23: note: Shadowed declaration z3-z3-4.13.3/src/ast/decl_collector.cpp:172:31: note: Shadow variable z3-z3-4.13.3/src/ast/ast.h:243:135: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:502:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_mark1_owner [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:868:85: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable symbol [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:1935:57: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:1944:59: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:1958:60: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2503:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2505:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2513:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2562:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2566:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:2575:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable IDX [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/ast.h:630:10: style:inconclusive: Technically the member function 'sort::set_num_elements' can be const. [functionConst] z3-z3-4.13.3/src/ast/ast.h:631:14: performance:inconclusive: Technically the member function 'sort::get_size' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:835:14: performance:inconclusive: Technically the member function 'var::get_size' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1583:10: performance:inconclusive: Technically the member function 'ast_manager::is_builtin_family_id' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1605:15: performance:inconclusive: Technically the member function 'ast_manager::get_basic_family_id' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1609:15: performance:inconclusive: Technically the member function 'ast_manager::get_user_sort_family_id' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1645:10: performance:inconclusive: Technically the member function 'ast_manager::inc_ref' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1705:15: performance:inconclusive: Technically the member function 'ast_manager::get_eq_op' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1736:10: performance:inconclusive: Technically the member function 'ast_manager::is_uninterp' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1738:10: performance:inconclusive: Technically the member function 'ast_manager::is_type_var' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1853:10: style:inconclusive: Technically the member function 'ast_manager::is_considered_uninterpreted' can be const. [functionConst] z3-z3-4.13.3/src/ast/ast.h:1975:10: performance:inconclusive: Technically the member function 'ast_manager::is_label' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1981:10: performance:inconclusive: Technically the member function 'ast_manager::is_label' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1997:10: performance:inconclusive: Technically the member function 'ast_manager::is_label_lit' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:1999:15: performance:inconclusive: Technically the member function 'ast_manager::get_label_family_id' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2117:10: performance:inconclusive: Technically the member function 'ast_manager::is_or' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2118:10: performance:inconclusive: Technically the member function 'ast_manager::is_implies' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2119:10: performance:inconclusive: Technically the member function 'ast_manager::is_and' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2120:10: performance:inconclusive: Technically the member function 'ast_manager::is_not' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2121:10: performance:inconclusive: Technically the member function 'ast_manager::is_eq' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2123:10: performance:inconclusive: Technically the member function 'ast_manager::is_oeq' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2124:10: performance:inconclusive: Technically the member function 'ast_manager::is_distinct' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2125:10: performance:inconclusive: Technically the member function 'ast_manager::is_xor' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2126:10: performance:inconclusive: Technically the member function 'ast_manager::is_ite' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2135:10: performance:inconclusive: Technically the member function 'ast_manager::is_or' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2136:10: performance:inconclusive: Technically the member function 'ast_manager::is_implies' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2137:10: performance:inconclusive: Technically the member function 'ast_manager::is_and' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2138:10: performance:inconclusive: Technically the member function 'ast_manager::is_not' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2139:10: performance:inconclusive: Technically the member function 'ast_manager::is_eq' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2141:10: performance:inconclusive: Technically the member function 'ast_manager::is_xor' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2142:10: performance:inconclusive: Technically the member function 'ast_manager::is_ite' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2144:10: performance:inconclusive: Technically the member function 'ast_manager::is_distinct' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2224:10: performance:inconclusive: Technically the member function 'ast_manager::is_model_value' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2225:10: performance:inconclusive: Technically the member function 'ast_manager::is_model_value' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2259:10: performance:inconclusive: Technically the member function 'ast_manager::is_asserted' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2260:10: performance:inconclusive: Technically the member function 'ast_manager::is_hypothesis' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2261:10: performance:inconclusive: Technically the member function 'ast_manager::is_goal' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2262:10: performance:inconclusive: Technically the member function 'ast_manager::is_modus_ponens' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2263:10: performance:inconclusive: Technically the member function 'ast_manager::is_reflexivity' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2264:10: performance:inconclusive: Technically the member function 'ast_manager::is_symmetry' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2265:10: performance:inconclusive: Technically the member function 'ast_manager::is_transitivity' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2266:10: performance:inconclusive: Technically the member function 'ast_manager::is_monotonicity' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2267:10: performance:inconclusive: Technically the member function 'ast_manager::is_quant_intro' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2268:10: performance:inconclusive: Technically the member function 'ast_manager::is_quant_inst' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2269:10: performance:inconclusive: Technically the member function 'ast_manager::is_distributivity' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2270:10: performance:inconclusive: Technically the member function 'ast_manager::is_and_elim' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2271:10: performance:inconclusive: Technically the member function 'ast_manager::is_not_or_elim' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2272:10: performance:inconclusive: Technically the member function 'ast_manager::is_rewrite' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2273:10: performance:inconclusive: Technically the member function 'ast_manager::is_rewrite_star' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2274:10: performance:inconclusive: Technically the member function 'ast_manager::is_unit_resolution' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2275:10: performance:inconclusive: Technically the member function 'ast_manager::is_lemma' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2278:10: performance:inconclusive: Technically the member function 'ast_manager::is_hyper_resolve' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2286:10: performance:inconclusive: Technically the member function 'ast_manager::is_def_intro' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2287:10: performance:inconclusive: Technically the member function 'ast_manager::is_apply_def' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2288:10: performance:inconclusive: Technically the member function 'ast_manager::is_skolemize' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2503:10: performance:inconclusive: Technically the member function 'ast_fast_mark::is_marked' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2504:10: performance:inconclusive: Technically the member function 'ast_fast_mark::reset_mark' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2562:10: performance:inconclusive: Technically the member function 'ast_ref_fast_mark::is_marked' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:2565:10: performance:inconclusive: Technically the member function 'ast_ref_fast_mark::reset_mark' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/ast.h:625:17: warning: The class 'sort' defines member function with name 'get_info' also defined in its parent class 'decl'. [duplInheritedMember] z3-z3-4.13.3/src/ast/ast.h:592:17: note: Parent function 'decl::get_info' z3-z3-4.13.3/src/ast/ast.h:625:17: note: Derived function 'sort::get_info' z3-z3-4.13.3/src/ast/ast.h:652:22: warning: The class 'func_decl' defines member function with name 'get_info' also defined in its parent class 'decl'. [duplInheritedMember] z3-z3-4.13.3/src/ast/ast.h:592:17: note: Parent function 'decl::get_info' z3-z3-4.13.3/src/ast/ast.h:652:22: note: Derived function 'func_decl::get_info' z3-z3-4.13.3/src/ast/ast.h:852:25: warning: The class 'quantifier' defines member variable with name 'm_kind' also defined in its parent class 'ast'. [duplInheritedMember] z3-z3-4.13.3/src/ast/ast.h:464:14: note: Parent variable 'ast::m_kind' z3-z3-4.13.3/src/ast/ast.h:852:25: note: Derived variable 'quantifier::m_kind' z3-z3-4.13.3/src/ast/ast.h:878:21: warning: The class 'quantifier' defines member function with name 'get_kind' also defined in its parent class 'ast'. [duplInheritedMember] z3-z3-4.13.3/src/ast/ast.h:509:14: note: Parent function 'ast::get_kind' z3-z3-4.13.3/src/ast/ast.h:878:21: note: Derived function 'quantifier::get_kind' z3-z3-4.13.3/src/ast/ast.h:75:5: style: Class 'ast_exception' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:271:5: style: Class 'decl_info' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:287:9: style: Struct 'iterator' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:322:5: style: Class 'sort_size' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:360:5: style: Class 'sort_info' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:408:5: style: Struct 'func_decl_info' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:500:5: style: Class 'ast' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:603:9: style: Struct 'iterator' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:688:5: style: Class 'expr' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:766:5: style: Class 'tmp_app' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:1531:5: style: Class 'ast_manager' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:1543:9: style: Struct 'suspend_trace' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:2558:5: style: Class 'ast_ref_fast_mark' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:2640:5: style: Class 'scoped_mark' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:2659:5: style: Class 'dec_ref_proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:2668:5: style: Class 'inc_ref_proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/display_dimacs.cpp:29:5: style: Struct 'dimacs_pp' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/ast.h:167:67: style: Return value 'i=get_int(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:168:69: style: Return value 'a=get_ast(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:169:79: style: Return value 's=get_symbol(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:170:87: style: Return value 'r=get_rational(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:171:79: style: Return value 'd=get_double(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:172:87: style: Return value 'id=get_ext_id(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:173:82: style: Return value 's=get_zstring(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:936:116: style: Return value 'idx=static_cast(n)->get_idx(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/ast.h:1872:43: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/ast.h:1884:43: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/ast.h:799:21: style: Parameter 'source' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:807:35: style: Parameter 'source' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:1633:36: style: Parameter 'q' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:1636:36: style: Parameter 'e' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:2278:34: style: Parameter 'p' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:2503:26: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/ast.h:2562:26: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/display_dimacs.cpp:167:18: style: Consider using std::accumulate algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/dl_decl_plugin.cpp:184:17: error: There is an unknown macro here somewhere. Configuration is required. If IF_VERBOSE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/euf/euf_ac_plugin.cpp:443:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/euf/euf_arith_plugin.cpp:29:75: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable undo_add [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_bv_plugin.cpp:528:17: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/euf/euf_egraph.cpp:110:9: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/euf/euf_enode.cpp:45:17: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:44:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable Z3_fallthrough [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:78:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable unary_table [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:114:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_func_decl2id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:120:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tables [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:144:31: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_func_decl2id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:214:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_commutativity [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:240:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:112:23: style: Local variable 'd' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:101:19: note: Shadowed declaration z3-z3-4.13.3/src/ast/euf/euf_etable.cpp:112:23: note: Shadow variable z3-z3-4.13.3/src/ast/euf/euf_justification.cpp:26:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_kind [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_plugin.cpp:29:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_plugin.cpp:34:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_plugin.cpp:46:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_region [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_specrel_plugin.cpp:46:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_plugins [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_specrel_plugin.cpp:51:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_plugins [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_specrel_plugin.cpp:56:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_plugins [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/euf/euf_specrel_plugin.cpp:67:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_plugins [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr2polynomial.cpp:371:17: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/expr2var.cpp:29:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/expr_abstract.cpp:113:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/expr_functors.cpp:72:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_check_quantifiers [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_functors.cpp:136:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_map.cpp:42:45: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_value [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_map.cpp:65:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_store_proofs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_map.cpp:75:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_store_proofs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_stat.cpp:30:16: style: Variable 'p' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/src/ast/expr_substitution.cpp:29:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_subst_pr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_substitution.cpp:61:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_subst [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_substitution.cpp:68:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable expr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/expr_substitution.cpp:159:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/for_each_expr.cpp:116:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_esp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/for_each_expr.cpp:140:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_include_bound [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/for_each_expr.cpp:195:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_include_bound [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/for_each_expr.cpp:65:23: style: Local variable 'rc' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/for_each_expr.cpp:50:15: note: Shadowed declaration z3-z3-4.13.3/src/ast/for_each_expr.cpp:65:23: note: Shadow variable z3-z3-4.13.3/src/ast/for_each_expr.cpp:25:27: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/for_each_expr.cpp:27:34: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/for_each_expr.cpp:93:31: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/for_each_expr.cpp:95:38: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/format.cpp:39:72: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable FORMAT_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:65:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable FORMAT_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:112:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable FORMAT_SORT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:128:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_LINE_BREAK [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:148:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_STRING [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:162:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_INDENT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:166:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_LINE_BREAK [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:170:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_CHOICE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:178:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_COMPOSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:182:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_COMPOSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:186:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_COMPOSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:191:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_COMPOSE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:195:37: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable OP_NIL [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/format.cpp:125:18: performance:inconclusive: Technically the member function 'format_ns::flat_visitor::visit' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/format.cpp:126:18: performance:inconclusive: Technically the member function 'format_ns::flat_visitor::visit' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/format.cpp:119:9: style: Struct 'flat_visitor' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/format.cpp:135:76: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/format.cpp:178:64: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/format.cpp:126:37: style: Parameter 'q' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/fpa/bv2fpa_converter.cpp:114:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/fpa/fpa2bv_converter.cpp:2440:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/fpa/fpa2bv_rewriter.cpp:57:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/fpa_decl_plugin.cpp:1068:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:45:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:63:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:70:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:74:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:200:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_deps [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:216:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:33:10: style:inconclusive: Technically the member function 'collect_dependencies_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:35:10: style:inconclusive: Technically the member function 'collect_dependencies_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:179:5: style: Class 'top_sort' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:33:27: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/func_decl_dependencies.cpp:35:34: style: Parameter 'n' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/has_free_vars.cpp:92:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/has_free_vars.cpp:96:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/has_free_vars.cpp:100:14: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/has_free_vars.cpp:24:1: style: The class 'imp' does not declare a constructor although it has private member variables which likely require initialization. [noConstructor] z3-z3-4.13.3/src/ast/macro_substitution.cpp:29:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_decl2macro_pr [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/macro_substitution.cpp:63:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/macro_substitution.cpp:85:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable quantifier [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/macros/macro_finder.cpp:28:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/macros/macro_manager.cpp:117:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/macros/macro_util.cpp:315:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/macros/quantifier_macro_info.cpp:32:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/macros/quantifier_macro_info.cpp:59:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_is_auf [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/macros/quasi_macros.cpp:160:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/normal_forms/defined_names.cpp:166:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/normal_forms/elim_term_ite.cpp:37:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/normal_forms/name_exprs.cpp:60:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/normal_forms/nnf.cpp:83:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/normal_forms/pull_quant.cpp:101:17: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/num_occurs.cpp:35:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_ignore_ref_count1 [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/num_occurs.cpp:63:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_occurs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/occurs.cpp:39:14: style:inconclusive: Technically the member function '::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:40:14: style:inconclusive: Technically the member function '::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:41:14: style:inconclusive: Technically the member function '::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:48:14: style:inconclusive: Technically the member function '::decl_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:49:14: style:inconclusive: Technically the member function '::decl_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:50:14: style:inconclusive: Technically the member function '::decl_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:57:14: style:inconclusive: Technically the member function '::sort_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:58:14: style:inconclusive: Technically the member function '::sort_proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/occurs.cpp:38:9: style: Struct 'proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/occurs.cpp:47:9: style: Struct 'decl_proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/occurs.cpp:56:9: style: Struct 'sort_proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/pattern/expr_pattern_match.cpp:102:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/pattern/pattern_inference.cpp:640:13: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:34:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_manager [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:92:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:111:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:128:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:144:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:166:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:180:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/pb_decl_plugin.cpp:316:48: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/polymorphism_inst.cpp:51:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_occurs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_inst.cpp:85:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_assertions_qhead [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_inst.cpp:107:41: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_instances [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:26:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:34:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:57:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:274:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:302:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:319:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:334:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:350:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:317:18: style:inconclusive: Technically the member function 'polymorphism::collect_poly_instances::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:332:18: style:inconclusive: Technically the member function 'polymorphism::has_type_vars::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:348:18: style:inconclusive: Technically the member function 'polymorphism::collect_type_vars::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:327:13: style: Struct 'proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:317:34: style: Parameter 'a' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:332:34: style: Parameter 'a' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/polymorphism_util.cpp:348:34: style: Parameter 'a' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/pp.cpp:55:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/proofs/proof_checker.cpp:1399:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/proofs/proof_utils.cpp:325:5: error: There is an unknown macro here somewhere. Configuration is required. If DEBUG_CODE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/quantifier_stat.cpp:46:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_case_split_factor [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/quantifier_stat.cpp:51:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_region [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/quantifier_stat.cpp:54:21: style: Variable 'e' can be declared as reference to const [constVariableReference] z3-z3-4.13.3/src/ast/recfun_decl_plugin.cpp:227:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/reg_decl_plugins.cpp:35:50: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable arith_decl_plugin [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/arith_rewriter.cpp:100:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/array_rewriter.cpp:118:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/ast_counter.cpp:83:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fv [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/ast_counter.cpp:42:13: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/rewriter/bit2int.cpp:41:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/bit_blaster/bit_blaster.cpp:41:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp:382:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/bool_rewriter.cpp:734:13: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/bv_bounds.cpp:25:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/bv_elim.cpp:22:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/bv_elim.cpp:49:22: style: Local variable 'bv' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/rewriter/bv_elim.cpp:27:22: note: Shadowed declaration z3-z3-4.13.3/src/ast/rewriter/bv_elim.cpp:49:22: note: Shadow variable z3-z3-4.13.3/src/ast/rewriter/bv_rewriter.cpp:244:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/cached_var_subst.cpp:68:9: error: There is an unknown macro here somewhere. Configuration is required. If SCTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:26:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_char [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:35:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:61:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:67:12: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:75:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_DONE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:92:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/char_rewriter.cpp:104:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/datatype_rewriter.cpp:25:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/datatype_rewriter.cpp:108:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/der.cpp:51:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/distribute_forall.cpp:158:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/dl_rewriter.cpp:31:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_DONE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/dom_simplifier.cpp:93:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/elim_bounds.cpp:154:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:94:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_DONE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:196:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable lambda_k [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:321:77: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:322:49: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:324:59: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:326:82: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_params [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:327:89: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_enum2bv [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:328:89: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_bv2enum [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:329:85: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_enum2def [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:330:94: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:334:67: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_translated [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/enum2bv_rewriter.cpp:275:10: performance:inconclusive: Technically the member function 'imp::updt_params' can be static (but you may consider moving to unnamed namespace). [functionStatic] z3-z3-4.13.3/src/ast/rewriter/expr_replacer.cpp:100:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_subst [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/expr_replacer.cpp:63:5: style: Struct 'default_expr_replacer_cfg' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/rewriter/expr_safe_replace.cpp:36:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/expr_safe_replace.cpp:60:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_cache [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/expr_safe_replace.cpp:199:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_limit [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/factor_equivs.cpp:89:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/factor_rewriter.cpp:198:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/fpa_rewriter.cpp:146:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/func_decl_replace.cpp:90:38: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/inj_axiom.cpp:78:21: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/label_rewriter.cpp:35:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_DONE [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/macro_replacer.cpp:44:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/macro_replacer.cpp:128:41: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/macro_replacer.cpp:42:83: style: Parameter 'result' can be declared as reference to const [constParameterReference] z3-z3-4.13.3/src/ast/rewriter/maximize_ac_sharing.cpp:49:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/mk_extract_proc.cpp:27:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_f_cached [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/mk_extract_proc.cpp:44:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_low [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/mk_simplified_app.cpp:48:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/mk_simplified_app.cpp:93:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_imp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/pb2bv_rewriter.cpp:160:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/pb_rewriter.cpp:322:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/push_app_ite.cpp:51:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/quant_hoist.cpp:47:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/recfun_rewriter.cpp:28:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable BR_FAILED [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/rewriter.cpp:53:5: error: There is an unknown macro here somewhere. Configuration is required. If CTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/seq_axioms.cpp:194:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:25:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:175:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:205:70: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:283:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:331:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:362:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:412:75: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:229:9: style: Consecutive return, break, continue, goto or throw statements are unnecessary. [duplicateBreak] z3-z3-4.13.3/src/ast/rewriter/seq_eq_solver.cpp:449:9: style: Consider using std::any_of algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/rewriter/seq_rewriter.cpp:254:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:25:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_prefix [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:54:55: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:61:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_max_unfolding [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:67:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_length_limit [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:118:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tail [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:163:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_left [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:177:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eq [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:181:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_pre [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:185:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_post [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:199:63: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:209:76: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:215:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:150:96: style: Return value 'idx=r.get_unsigned(),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:159:81: style: Return value 's=to_app(e)->get_arg(0),idx=to_app(e)->get_arg(1),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:177:87: style: Return value 'a=to_app(e)->get_arg(0),b=to_app(e)->get_arg(1),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:181:88: style: Return value 's=to_app(e)->get_arg(0),i=to_app(e)->get_arg(1),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:185:93: style: Return value 's=to_app(e)->get_arg(0),start=to_app(e)->get_arg(1),true' is always true [knownConditionTrueFalse] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:191:15: warning:inconclusive: Possible null pointer dereference: u [nullPointer] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:189:15: note: Assignment 'u=nullptr', assigned value is 0 z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:191:15: note: Null pointer dereference z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:62:83: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:68:83: style: C-style pointer casting [cstyleCast] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:119:15: style: Local variable 's' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:87:13: note: Shadowed declaration z3-z3-4.13.3/src/ast/rewriter/seq_skolem.cpp:119:15: note: Shadow variable z3-z3-4.13.3/src/ast/rewriter/th_rewriter.cpp:551:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/value_sweep.cpp:114:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/rewriter/var_subst.cpp:34:9: error: There is an unknown macro here somewhere. Configuration is required. If SCTRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/seq_decl_plugin.cpp:73:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/shared_occs.cpp:25:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_shared [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/shared_occs.cpp:46:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_track_atomic [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/shared_occs.cpp:108:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_visit_quantifiers [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/shared_occs.cpp:135:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_shared [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/shared_occs.cpp:144:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_shared [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/shared_occs.cpp:144:16: style: Variable 's' can be declared as pointer to const [constVariablePointer] z3-z3-4.13.3/src/ast/shared_occs.cpp:144:37: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/simplifiers/bit_blaster.cpp:46:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/bound_manager.cpp:110:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/bound_propagator.cpp:274:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:61:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_interval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:145:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fmls [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:277:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_interval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:290:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:298:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:305:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_interval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:316:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_interval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:327:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_interval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:425:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:453:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:466:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:474:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable nm [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:44:5: style: Struct 'rw_cfg' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:52:5: style: Struct 'rw' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:139:26: style: The scope of the variable 'found_bound' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:253:11: style: The scope of the variable 'z' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:253:16: style: The scope of the variable 'u' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:253:21: style: The scope of the variable 'v' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:253:26: style: The scope of the variable 'w' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:254:10: style: The scope of the variable 'strict' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:475:30: style: The scope of the variable 'has_l' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:475:37: style: The scope of the variable 'has_u' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:279:24: style: Local variable 'k' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:251:17: note: Shadowed declaration z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:279:24: note: Shadow variable z3-z3-4.13.3/src/ast/simplifiers/bound_simplifier.cpp:139:38: style: Variable 'found_bound' is assigned a value that is never used. [unreadVariable] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:32:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_propagate_eq [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:36:34: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable CPK_BOOL [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:44:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:64:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable dominator_simplifier [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:31:10: style: Virtual function 'updt_params' is called from constructor 'dom_bv_bounds_simplifier(ast_manager&m,const params_ref&p)' at line 25. Dynamic binding is not used. [virtualCallInConstructor] z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:25:9: note: Calling updt_params z3-z3-4.13.3/src/ast/simplifiers/bv_bounds_simplifier.cpp:31:10: note: updt_params is a virtual function z3-z3-4.13.3/src/ast/simplifiers/bv_slice.cpp:31:36: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fmls [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_slice.cpp:44:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_xs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_slice.cpp:54:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_xs [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/bv_slice.cpp:136:31: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/card2bv.cpp:30:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/card2bv.cpp:54:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_rewrites [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/card2bv.cpp:58:46: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable CPK_BOOL [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/demodulator_simplifier.cpp:119:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:78:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_recfun [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:97:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_lambdas [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:122:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_suffix_frozen [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:143:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_has_quantifiers [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:62:14: style:inconclusive: Technically the member function 'freeze_terms::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/simplifiers/dependent_expr_state.cpp:62:30: style: Parameter 's' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/simplifiers/distribute_forall.cpp:94:16: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/distribute_forall.cpp:25:5: style: Struct 'rw_cfg' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/dominator_simplifier.cpp:63:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/elim_unconstrained.cpp:83:9: error: There is an unknown macro here somewhere. Configuration is required. If IF_VERBOSE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:68:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_bound [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:178:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:219:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:308:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:316:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:335:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:350:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:413:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:606:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_predicates [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:613:18: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:622:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:657:30: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable tout [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:710:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:754:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:788:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:833:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_predicates [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:855:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_to_exclude [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:862:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fmls [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:877:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:905:24: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_disable_elimination [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:941:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable func_decl [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:979:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_clauses [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:1004:31: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_macros [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:851:14: style:inconclusive: Technically the member function 'process_to_exclude::proc::operator()' can be const. [functionConst] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:845:9: style: Struct 'proc' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:596:15: style: Local variable 'x' shadows outer variable [shadowVariable] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:363:11: note: Shadowed declaration z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:596:15: note: Shadow variable z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:851:30: style: Parameter 's' can be declared as pointer to const [constParameterPointer] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:652:15: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:655:15: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:717:15: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/simplifiers/eliminate_predicates.cpp:720:15: style: Consider using std::count_if algorithm instead of a raw loop. [useStlAlgorithm] z3-z3-4.13.3/src/ast/simplifiers/euf_completion.cpp:361:13: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:36:9: style: Class 'basic_extract_eq' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:266:9: style: Class 'arith_extract_eq' has a constructor with 1 argument that is not explicit. [noExplicitConstructor] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:55:36: style: The scope of the variable 'x1' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:55:42: style: The scope of the variable 'y1' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:55:48: style: The scope of the variable 'x2' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/extract_eqs.cpp:55:54: style: The scope of the variable 'y2' can be reduced. [variableScope] z3-z3-4.13.3/src/ast/simplifiers/linear_equation.cpp:99:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/max_bv_sharing.cpp:49:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/model_reconstruction_trail.cpp:39:5: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/propagate_values.cpp:38:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fmls [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/propagate_values.cpp:75:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_fmls [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/propagate_values.cpp:107:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_num_rewrites [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/propagate_values.cpp:112:5: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_max_rounds [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/propagate_values.cpp:118:28: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable CPK_UINT [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/simplifiers/reduce_args_simplifier.cpp:129:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/solve_context_eqs.cpp:239:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/simplifiers/solve_eqs.cpp:191:9: error: There is an unknown macro here somewhere. Configuration is required. If TRACE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/sls/bv_sls.cpp:285:13: error: There is an unknown macro here somewhere. Configuration is required. If IF_VERBOSE is a macro then please configure it. [unknownMacro] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:34:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable basic_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:67:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_todo [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:99:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable sls_valuation [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:146:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable basic_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:215:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable basic_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:236:25: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:298:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable basic_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:307:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_values [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:324:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable null_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:699:43: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:705:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable basic_family_id [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:863:42: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:887:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:893:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:903:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:920:33: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:945:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:953:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:978:9: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:991:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1002:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1008:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1019:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1030:27: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1054:48: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1150:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1157:26: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1170:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_b [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1196:20: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_b [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1231:47: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1252:22: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp4 [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1275:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_zero [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1283:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1297:52: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1330:39: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1367:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1446:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1499:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1561:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1620:21: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1681:23: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1725:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp3 [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1732:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp3 [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1755:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1769:19: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1778:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1809:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1823:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1833:35: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_tmp [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1851:29: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_prob_randomize_extract [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1875:40: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable digit_t [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1900:13: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_eval [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1921:17: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_values [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1944:32: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m_rand [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1975:54: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1987:60: debug: valueFlowConditionExpressions bailout: Skipping function due to incomplete variable m [valueFlowBailoutIncompleteVar] z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1389:25: style: Condition 'sh=b.bw' is not redundant z3-z3-4.13.3/src/ast/sls/bv_sls_eval.cpp:1389:25: note: Condition 'sh=src_sz' is not redundant z3-z3-4.13.3/src/util/bit_util.cpp:142:24: note: Condition 'dst_sz