atlas.properties

# Logging
# See http://www.slf4j.org/api/org/slf4j/impl/SimpleLogger.html
org.slf4j.simpleLogger.dateTimeFormat=yyyy-MM-dd'T'HH:mm:ss.SSSZ
org.slf4j.simpleLogger.defaultLogLevel=debug
org.slf4j.simplelogger.levelInBrackets=true
org.slf4j.simpleLogger.logFile=atlas.log
org.slf4j.simpleLogger.showDateTime=true
org.slf4j.simpleLogger.showLogName=true
org.slf4j.simpleLogger.showThreadName=true

# Z3
# Configuration properties for Z3 must be prefixed with `com.microsoft.z3`.
# A list can be obtained by running `z3 -p` in a shell. The complete list
# of parameters is very long. The most important ones are global parameters:
# auto_config (bool) (default: true)
# debug_ref_count (bool) (default: false)
# dot_proof_file (string) (default: proof.dot)
# dump_models (bool) (default: false)
# memory_high_watermark (unsigned int) (default: 0)
# memory_max_alloc_count (unsigned int) (default: 0)
# memory_max_size (unsigned int) (default: 0) [bytes]
# model (bool) (default: true)
# model_validate (bool) (default: false)
# proof (bool) (default: false)
# rlimit (unsigned int) (default: 0)
# smtlib2_compliant (bool) (default: false)
# stats (bool) (default: false)
# timeout (unsigned int) (default: 4294967295) [milliseconds]
# trace (bool) (default: false)
# trace_file_name (string) (default: z3.log)
# type_check (bool) (default: true)
# unsat_core (bool) (default: false)
# verbose (unsigned int) (default: 0)
# warning (bool) (default: true)
# well_sorted_check (bool) (default: false)
# Timeout 15M
#com.microsoft.z3.timeout=900000
# Timeout 2H
com.microsoft.z3.timeout=7200000
com.microsoft.z3.memory_max_size=25769803776
com.microsoft.z3.unsat_core=true
com.microsoft.z3.trace=false

# TODO
#com.microsoft.z3.parallel.enable=true
#com.microsoft.z3.parallel.threads.max=4