mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-10 16:13:25 +00:00
Code Activity

Fix non ASCII character

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-24 08:59:43 -07:00
parent 7c3ca302f0
commit 2633dc56ab
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/mk_util.py
View file

@ -520,6 +520,7 @@ def parse_options():
# Return a list containing a file names included using '#include' in # Return a list containing a file names included using '#include' in
# the given C/C++ file named fname. # the given C/C++ file named fname.
def extract_c_includes(fname): def extract_c_includes(fname):
print(fname)
result = [] result = []
# We look for well behaved #include directives # We look for well behaved #include directives
std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")

2
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -11,7 +11,7 @@ Abstract:
The linear invariants are extracted according to Karr's method. The linear invariants are extracted according to Karr's method.
A short description is in A short description is in
Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation Nikolaj Bjorner, Anca Browne and Zohar Manna. Automatic Generation
of Invariants and Intermediate Assertions, in CP 95. of Invariants and Intermediate Assertions, in CP 95.
The algorithm is here adapted to Horn clauses. The algorithm is here adapted to Horn clauses.