diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f3d9a5169..10b6888c9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1017,6 +1017,7 @@ public: void apply_sort_cnstr(enode* n, sort*) { TRACE(arith, tout << "sort constraint: " << pp(n) << "\n";); + std::cout << "sort constraint: " << pp(n) << " " << __FILE__ << ":" << __LINE__ << "\n"; #if 0 if (!th.is_attached_to_var(n)) mk_var(n->get_owner()); diff --git a/sus.py b/sus.py new file mode 100644 index 000000000..4db234483 --- /dev/null +++ b/sus.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 +""" +sus.py: Search for function calls with three function-call arguments (ambiguous parameter evaluation order) +and print matches in grep-like format: file:line:match +""" +import os +import re + +# pattern: identifier(... foo(...), ... bar(...)) with two function-call args +pattern = re.compile( + r"\b[A-Za-z_]\w*" # function name + r"\s*\(\s*" # '(' + r"[^)]*?[A-Za-z_]\w*\([^)]*\)" # first func-call arg anywhere + r"[^)]*?,[^)]*?[A-Za-z_]\w*\([^)]*\)" # second func-call arg + r"[^)]*?\)" # up to closing ')' +) + +# file extensions to include +excl = ('TRACE', 'ASSERT', 'VERIFY', ) + +for root, dirs, files in os.walk('src/smt'): + # skip hidden dirs + dirs[:] = [d for d in dirs if not d.startswith('.')] + for file in files: + path = os.path.join(root, file) + try: + with open(path, 'r', encoding='utf-8', errors='ignore') as f: + for i, line in enumerate(f, 1): + if pattern.search(line): + # skip lines with TRACE or ASSERT in all caps + if any(word in line for word in excl): + continue + full_path = os.path.abspath(path) + print(f"{full_path}:{i}:{line.rstrip()}") + except OSError: + pass