forked from jwiesler/ips4o-verify
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathproofIndependentSettings.props
72 lines (72 loc) · 3.34 KB
/
proofIndependentSettings.props
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
#Proof-Independent-Settings-File. Generated Fri Oct 27 16:18:59 CEST 2023
#Fri Oct 27 16:18:59 CEST 2023
[General]UseJML=true
[SMTSettings]solverParametersV1CVC4=\#beg--no-print-success -m --interactive --lang smt2\#end
[View][Heatmap]maxAge=5
[View]SequentViewTooltips=true
[General]RightClickMacros=true
[View]HideIntermediateProofsteps=false
[SMTSettings]solverCommandZ3\ FP=\#begz3\#end
[View][Heatmap]newest=true
[View]ShowWholeTaclet=false
[View]SourceViewTooltips=true
[View]showUninstantiatedTaclet=true
[View][Heatmap]sf=true
[SMTSettings]objectBound=3
[View]HighlightOrigin=true
[General]DnDDirectionSensitive=true
[SMTSettings]solverParametersV1Z3=\#beg-in -smt2\#end
[View]UseSystemLookAndFeel=false
[View]ShowLoadExamplesDialog=true
[SMTSettings]fieldBound=3
[SMTSettings]SolverTimeout=20000
[View]UseUnicodeSymbols=false
[View]SyntaxHighlighting=true
[View]hideInteractiveGoals=false
[Extensions]disabled=
[SMTSettings]intBound=3
[General]StupidMode=true
[SMTSettings]solverParametersV1Z3\ FP=\#beg-in -smt2\#end
[SMTSettings]timeoutZ3\ FP=-1
[SMTSettings]solverCommandZ3_CE=\#begz3\#end
[SMTSettings]solverCommandZ3\ (Legacy\ Translation)=\#begz3\#end
[SMTSettings]solverParametersV1CVC4\ (Legacy\ Translation)=\#beg--no-print-success -m --interactive --lang smt2\#end
[View]ConfirmExit=true
[SMTSettings]ActiveSolver=\#begZ3\#end
[View]clutterRules=add_eq,add_greatereq,add_lesseq,add_non_neq_square,apply_eq_monomialseqTermCut,boxToDiamond,case_distinction_l,case_distinction_r,commute_and_2,commute_or_2,cut_direct_l,cut_direct_r,divIncreasingNeg,divIncreasingPos,divide_equation,divide_geq,equal_add_one,geq_add_one,instAll,instEx,jdivAddMultDenom,jmodAltZero,jmodDivisble,jmodUnique1,jmodeUnique2,jmodjmod,leq_add_one,less_is_total,less_zero_is_total,local_cut,polySimp_addOrder,polySimp_expand,pullOut,typeStatic
[SMTSettings]solverCommandINVISMT=\#beginvismt\#end
[View]HideClosedSubtrees=false
[View]FontIndex=2
[SMTSettings]solverParametersV1Z3_CE=\#beg-in -smt2\#end
[SMTSettings]checkForSupport=true
[View]uiFontSizeFactor=1.0
[View]HideAutomodeProofsteps=false
[View][Heatmap]enabled=false
[SMTSettings]solverParametersV1Z3\ (Legacy\ Translation)=\#beg-in -smt2\#end
[View]clutterRuleSets=inEqSimp_commute,inEqSimp_expand,inEqSimp_nonLin,inEqSimp_nonLin_divide,inEqSimp_special_nonLin,notHumanReadable,obsolete,polySimp_directEquations,polySimp_normalise,pullOutQuantifierAll,pullOutQuantifierEx
[General]AutoSavePeriod=0
[SMTSettings]solverCommandZ3=\#begz3\#end
[General]EnsureSourceConsistency=true
[SMTSettings]locsetBound=3
[SMTSettings]solverCommandCVC4=\#begcvc4\#end
[SMTSettings]pathForSMTTranslation=\#beg\#end
[SMTSettings]timeoutZ3_CE=-1
[View]notifyLoadBehaviour=false
[View]folderBookmarks=/home/mattias
[View]PrettySyntax=true
[SMTSettings]solverCommandCVC4\ (Legacy\ Translation)=\#begcvc4\#end
[SMTSettings]timeoutZ3\ (Legacy\ Translation)=-1
[SMTSettings]maxConcurrentProcesses=2
[SMTSettings]timeoutCVC4\ (Legacy\ Translation)=-1
[SMTSettings]showSMTResDialog=false
[SMTSettings]solverParametersV1INVISMT=\#beg-in\#end
[SMTSettings]timeoutCVC4=-1
[SMTSettings]timeoutINVISMT=-1
[SMTSettings]modeOfProgressDialog=0
[SMTSettings]pathForTacletTranslation=\#beg\#end
[View]MaxTooltipLines=40
[SMTSettings]timeoutZ3=-1
[LemmaGenerator]showDialogWhenUsingTacletsAsAxioms=true
[View]HidePackagePrefix=false
[LemmaGenerator]showDialogWhenAddingAxioms=true
[SMTSettings]heapBound=3