diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5b7c10605..820396c0d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -553,7 +553,7 @@ def display_help(exit_code): if IS_WINDOWS: print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") if IS_WINDOWS: - print(" --optimize generate optimized code during linking.") + print(" --optimize generate optimized code during linking.") print(" -j, --java generate Java bindings.") print(" --ml generate OCaml bindings.") print(" --staticlib build Z3 static library.") @@ -621,8 +621,8 @@ def parse_options(): DOTNET_ENABLED = False elif opt in ('--staticlib'): STATIC_LIB = True - elif opt in ('--optimize'): - OPTIMIZE = True + elif opt in ('--optimize'): + OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): PREFIX = arg PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages') @@ -1786,8 +1786,8 @@ def mk_config(): 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: # Windows Release mode - if OPTIMIZE: - config.write('AR_FLAGS=/nologo /LTCG\n') + if OPTIMIZE: + config.write('AR_FLAGS=/nologo /LTCG\n') config.write( 'LINK_FLAGS=/nologo /MD\n' 'SLINK_FLAGS=/nologo /LD\n') diff --git a/src/api/python/z3util.py b/src/api/python/z3util.py index 6cdd4de32..e0e9aba32 100644 --- a/src/api/python/z3util.py +++ b/src/api/python/z3util.py @@ -210,18 +210,18 @@ def prove(claim,assume=None,verbose=0): if verbose >= 2: - print 'assume: ' - print assume - print 'claim: ' - print claim - print 'to_prove: ' - print to_prove + print('assume: ') + print(assume) + print('claim: ') + print(claim) + print('to_prove: ') + print(to_prove) f = Not(to_prove) models = get_models(f,k=1) if models is None: #unknown - print 'E: cannot solve !' + print('E: cannot solve !') return None, None elif models == False: #unsat return True,None @@ -458,7 +458,7 @@ def model_str(m,as_str=True): if m : vs = [(v,m[v]) for v in m] - vs = sorted(vs,key=lambda (a,_): str(a)) + vs = sorted(vs,key=lambda a,_: str(a)) if as_str: return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs]) else: