Bug: same conditions found. It is very likely a copy-paste bug. #4668
Assignees
Comments
NikolajBjorner
added a commit
that referenced
this issue
Sep 8, 2020
* fixing issue #4651 * regression fix * fix #4662 Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * Allow to skip System.loadLibrary() calls from Java Native class (#4667) * using intended utility methods for sort detection * adding ack/model Signed-off-by: Nikolaj Bjorner <[email protected]> * add smt params dependency Signed-off-by: Nikolaj Bjorner <[email protected]> * missing file Signed-off-by: Nikolaj Bjorner <[email protected]> * deps Signed-off-by: Nikolaj Bjorner <[email protected]> * order Signed-off-by: Nikolaj Bjorner <[email protected]> * persist fields Signed-off-by: Nikolaj Bjorner <[email protected]> * dbg build Signed-off-by: Nikolaj Bjorner <[email protected]> * reset caches Signed-off-by: Nikolaj Bjorner <[email protected]> * sr Signed-off-by: Nikolaj Bjorner <[email protected]> * fix cmake build Signed-off-by: Nikolaj Bjorner <[email protected]> * shuffle dependencies Signed-off-by: Nikolaj Bjorner <[email protected]> * warnings /errors Signed-off-by: Nikolaj Bjorner <[email protected]> * update include Signed-off-by: Nikolaj Bjorner <[email protected]> * missing cmakelists Signed-off-by: Nikolaj Bjorner <[email protected]> * update cmake Signed-off-by: Nikolaj Bjorner <[email protected]> * add depend Signed-off-by: Nikolaj Bjorner <[email protected]> * add depend Signed-off-by: Nikolaj Bjorner <[email protected]> * virtual method Signed-off-by: Nikolaj Bjorner <[email protected]> * path Signed-off-by: Nikolaj Bjorner <[email protected]> * move parameters from ast/rewriter to params Signed-off-by: Nikolaj Bjorner <[email protected]> * move fpa Signed-off-by: Nikolaj Bjorner <[email protected]> * fix warnings Signed-off-by: Nikolaj Bjorner <[email protected]> * remove pragma Signed-off-by: Nikolaj Bjorner <[email protected]> * dbg Signed-off-by: Nikolaj Bjorner <[email protected]> * updated sat_smt Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * fix #4651 Signed-off-by: Nikolaj Bjorner <[email protected]> * encoding options #4665 Signed-off-by: Nikolaj Bjorner <[email protected]> * expose name inclusion as optional Signed-off-by: Nikolaj Bjorner <[email protected]> * fix misc issues around #4661 introduced when adding lazy push/pop to selected theories Signed-off-by: Nikolaj Bjorner <[email protected]> * remove lazy push from theory_lra Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * fix dotnet build Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * release nodes Signed-off-by: Nikolaj Bjorner <[email protected]> * free memory in egraph Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid duplicate class names frame in sat_scc and sat_smt Signed-off-by: Nikolaj Bjorner <[email protected]> * adding euf Signed-off-by: Nikolaj Bjorner <[email protected]> * elaborate on smt/drat format outline, expose euf mode as config Signed-off-by: Nikolaj Bjorner <[email protected]> * mk-var during copy Signed-off-by: Nikolaj Bjorner <[email protected]> * move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph Signed-off-by: Nikolaj Bjorner <[email protected]> * with bounded Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * Remove duplicate binary condition. Fixes #4668. * butterfly effect on fp? Signed-off-by: Nikolaj Bjorner <[email protected]> * prepare for theory plugins Signed-off-by: Nikolaj Bjorner <[email protected]> * file Signed-off-by: Nikolaj Bjorner <[email protected]> * build fix * remove SMTFD Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * SMTFD is back (#4676) * fixing issue #4651 * regression fix * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * using intended utility methods for sort detection * misc edits related to nonground regexes * bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph * removed unused method declaration * improved id to regex value map info in generated dgml * reorgd callback function for state pretty printer * updated some comments Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Sergey Vladimirov <[email protected]> Co-authored-by: Christoph M. Wintersteiger <[email protected]> Co-authored-by: Arie Gurfinkel <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
z3/src/util/hwf.cpp
Line 345 in fa9cf0f
Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-2.3: LHS and RHS of a logical binary-operator (&&, ||), relational/equality binary-operator expression should not contain the same sub-expression.)
The text was updated successfully, but these errors were encountered: