Commit ba3984f9 authored by François Bobot's avatar François Bobot

try parameters given by Nikolaj Bjorner

parent acbaa9b7
......@@ -124,7 +124,26 @@ version_old = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 %f"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 \
PHASE_SELECTION=0 \
RESTART_STRATEGY=0 \
RESTART_FACTOR=1.5 \
QI_EAGER_THRESHOLD=100 \
ARITH_RANDOM_INITIAL_VALUE=true \
SORT_AND_OR=false \
CASE_SPLIT=3 \
DELAY_UNITS=true \
DELAY_UNITS_THRESHOLD=16 \
%f"
#Other Parameters given by Nikolaj Bjorner
#BV_REFLECT=true #arith?
#MODEL_PARTIAL=true
#MODEL_VALUE_COMPLETION=false
#MODEL_HIDE_UNUSED_PARTITIONS=false
#MODEL_V1=true
#ASYNC_COMMANDS=false
#NNF_SK_HACK=true
driver = "drivers/z3_smtv2_array.drv"
[ATP z3]
......
......@@ -330,6 +330,8 @@ and string_val key = parse
| '\\' 'n'
{ Buffer.add_char buf '\n';
string_val key lexbuf }
| '\\' '\n'
{ string_val key lexbuf }
| '\\' (_ as c)
{ Buffer.add_char buf '\\';
Buffer.add_char buf c;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment