Dynamic symbolic execution (DSE) is an effective method for automated program testing and bug detection. It is increasing the code coverage by the complex branches exploration during hybrid fuzzing. DSE tools invert the branches along some execution path and help fuzzer examine previously unavailable program parts. DSE often faces over- and underconstraint problems. The first one leads to significant analysis complication while the second one causes inaccurate symbolic execution. We propose strong optimistic solving method that eliminates irrelevant path predicate constraints for target branch inversion. We eliminate such symbolic constraints that the target branch is not control dependent on. Moreover, we separately handle symbolic branches that have nested control transfer instructions that pass control beyond the parent branch scope, e.g. return, goto, break, etc. We implement the proposed method in our dynamic symbolic execution tool Sydr. We evaluate the strong optimistic strategy, the optimistic strategy that contains only the last constraint negation, and their combination. The results show that the strategies combination helps increase either the code coverage or the average number of correctly inverted branches per one minute. It is optimal to apply both strategies together in contrast with other configurations.

翻译：动态符号执行( DSE) 是自动程序测试和错误检测的有效方法 。 它正在增加混合模糊过程中复杂分支勘探的代码范围 。 DSE 工具在一些执行路径上将分支倒转, 并帮助模糊者检查以前没有的程序部件 。 DSE 经常面临过度和不严格的问题 。 第一个导致分析严重复杂, 而第二个则造成不准确的符号执行。 我们建议了强烈乐观的解决方案, 消除目标分支倒转的不相关路径上游限制 。 我们消除了目标分支无法控制的这种象征性限制 。 此外, 我们单独处理已经嵌入控制控制指令的符号性分支, 这些指令超越了父分支范围, 例如 返回、 goto、 打破等 。 我们在动态符号执行工具 Sydr 中应用了拟议的方法 。 我们评估了强力的乐观战略, 乐观战略只包含最后的抑制否定, 及其组合 。 结果显示, 战略组合有助于增加代码覆盖或每分钟正确反转分支的平均数量 。 最理想的做法是将两种战略与其他配置一起应用 。