rewrite files

Author: wadoon

key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key

@@ -1,42 +1,75 @@
 \profile "Java Profile";
 
 \settings {
-"#Proof-Settings-Config-File
-#Wed Jun 04 18:23:41 CEST 2014
-[StrategyProperty]VBT_PHASE=VBT_SYM_EX
-[SMTSettings]useUninterpretedMultiplication=true
-[SMTSettings]SelectedTaclets=
-[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
-[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
-[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
-[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
-[SMTSettings]instantiateHierarchyAssumptions=true
-[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
-[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
-[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
-[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
-[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
-[Strategy]Timeout=-1
-[Strategy]MaximumNumberOfAutomaticApplications=10000
-[SMTSettings]integersMaximum=2147483645
-[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
-[SMTSettings]useConstantsForBigOrSmallIntegers=true
-[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
-[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
-[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
-[SMTSettings]maxGenericSorts=2
-[SMTSettings]integersMinimum=-2147483645
-[SMTSettings]invariantForall=false
-[SMTSettings]UseBuiltUniqueness=false
-[SMTSettings]explicitTypeHierarchy=false
-[Strategy]ActiveStrategy=JavaCardDLStrategy
-[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
-"
+    "Choice" : {
+        "JavaCard" : "JavaCard\:on",
+        "Strings" : "Strings\:on",
+        "assertions" : "assertions\:on",
+        "bigint" : "bigint\:on",
+        "initialisation" : "initialisation\:disableStaticInitialisation",
+        "intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules\:full",
+        "javacard" : "javacard:jcOff",
+        "modelFields" : "modelFields\:treatAsAxiom",
+        "nullPointerPolicy" : "nullPointerPolicy:nullCheck",
+        "programRules" : "programRules\:Java",
+        "reach" : "reach\:on",
+        "runtimeExceptions" : "runtimeExceptions\:ban",
+        "sequences" : "sequences\:on",
+        "stringRules" : "stringRules:withoutStringPool",
+        "throughout" : "throughout:toutOn",
+        "transactionAbort" : "transactionAbort:abortOn",
+        "transactions" : "transactions:transactionsOn",
+        "wdChecks" : "wdChecks\:off",
+        "wdOperator" : "wdOperator\:L"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+        
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+            
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
 }
 
 \javaSource "%%JAVA_SOURCE%%";

key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest.proof

@@ -1,45 +1,81 @@
 \profile "Java Profile for Symbolic Execution";
 
 \settings {
-"#Proof-Settings-Config-File
-#Tue Jul 25 22:57:12 CEST 2023
-[Choice]DefaultChoices=JavaCard-JavaCard\\:off, Strings-Strings\\:on, assertions-assertions\\:on, bigint-bigint\\:on, floatRules-floatRules\\:strictfpOnly, initialisation-initialisation\\:disableStaticInitialisation, intRules-intRules\\:arithmeticSemanticsIgnoringOF, integerSimplificationRules-integerSimplificationRules\\:full, javaLoopTreatment-javaLoopTreatment\\:efficient, mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off, methodExpansion-methodExpansion\\:noRestriction, modelFields-modelFields\\:showSatisfiability, moreSeqRules-moreSeqRules\\:off, permissions-permissions\\:off, programRules-programRules\\:Java, reach-reach\\:on, runtimeExceptions-runtimeExceptions\\:allow, sequences-sequences\\:on, wdChecks-wdChecks\\:off, wdOperator-wdOperator\\:L
-[Labels]UseOriginLabels=true
-[SMTSettings]SelectedTaclets=
-[SMTSettings]UseBuiltUniqueness=false
-[SMTSettings]explicitTypeHierarchy=false
-[SMTSettings]instantiateHierarchyAssumptions=true
-[SMTSettings]integersMaximum=2147483645
-[SMTSettings]integersMinimum=-2147483645
-[SMTSettings]invariantForall=false
-[SMTSettings]maxGenericSorts=2
-[SMTSettings]useConstantsForBigOrSmallIntegers=true
-[SMTSettings]useUninterpretedMultiplication=true
-[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
-[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
-[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
-[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
-[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
-[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
-[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
-[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
-[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_INSTANTIATE
-[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
-[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_RESTRICTED
-[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
-[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
-[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
-[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
-[StrategyProperty]VBT_PHASE=VBT_SYM_EX
-[Strategy]ActiveStrategy=Symbolic Execution Strategy
-[Strategy]MaximumNumberOfAutomaticApplications=500
-[Strategy]Timeout=-1
-"
+    "Choice" : {
+        "JavaCard" : "JavaCard\:off",
+        "Strings" : "Strings\:on",
+        "assertions" : "assertions\:on",
+        "bigint" : "bigint\:on",
+        "floatRules" : "floatRules\:strictfpOnly",
+        "initialisation" : "initialisation\:disableStaticInitialisation",
+        "intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules\:full",
+        "javaLoopTreatment" : "javaLoopTreatment\:efficient",
+        "javacard" : "javacard:jcOff",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal\:off",
+        "methodExpansion" : "methodExpansion\:noRestriction",
+        "modelFields" : "modelFields\:showSatisfiability",
+        "moreSeqRules" : "moreSeqRules\:off",
+        "nullPointerPolicy" : "nullPointerPolicy:nullCheck",
+        "permissions" : "permissions\:off",
+        "programRules" : "programRules\:Java",
+        "reach" : "reach\:on",
+        "runtimeExceptions" : "runtimeExceptions\:allow",
+        "sequences" : "sequences\:on",
+        "stringRules" : "stringRules:withoutStringPool",
+        "throughout" : "throughout:toutOn",
+        "transactionAbort" : "transactionAbort:abortOn",
+        "transactions" : "transactions:transactionsOn",
+        "wdChecks" : "wdChecks\:off",
+        "wdOperator" : "wdOperator\:L"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+        
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+            
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "Symbolic Execution Strategy",
+        "MaximumNumberOfAutomaticApplications" : 500,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_OFF",
+            "LOOP_OPTIONS_KEY" : "LOOP_EXPAND",
+            "METHOD_OPTIONS_KEY" : "METHOD_EXPAND",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_INSTANTIATE",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
 }
 
 \javaSource ".";

key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof

@@ -1,45 +1,81 @@
 \profile "Java Profile for Symbolic Execution";
 
 \settings {
-"#Proof-Settings-Config-File
-#Tue Jul 25 22:57:42 CEST 2023
-[Choice]DefaultChoices=JavaCard-JavaCard\\:off, Strings-Strings\\:on, assertions-assertions\\:on, bigint-bigint\\:on, floatRules-floatRules\\:strictfpOnly, initialisation-initialisation\\:disableStaticInitialisation, intRules-intRules\\:arithmeticSemanticsIgnoringOF, integerSimplificationRules-integerSimplificationRules\\:full, javaLoopTreatment-javaLoopTreatment\\:efficient, mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off, methodExpansion-methodExpansion\\:noRestriction, modelFields-modelFields\\:showSatisfiability, moreSeqRules-moreSeqRules\\:off, permissions-permissions\\:off, programRules-programRules\\:Java, reach-reach\\:on, runtimeExceptions-runtimeExceptions\\:allow, sequences-sequences\\:on, wdChecks-wdChecks\\:off, wdOperator-wdOperator\\:L
-[Labels]UseOriginLabels=true
-[SMTSettings]SelectedTaclets=
-[SMTSettings]UseBuiltUniqueness=false
-[SMTSettings]explicitTypeHierarchy=false
-[SMTSettings]instantiateHierarchyAssumptions=true
-[SMTSettings]integersMaximum=2147483645
-[SMTSettings]integersMinimum=-2147483645
-[SMTSettings]invariantForall=false
-[SMTSettings]maxGenericSorts=2
-[SMTSettings]useConstantsForBigOrSmallIntegers=true
-[SMTSettings]useUninterpretedMultiplication=true
-[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
-[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
-[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
-[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
-[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
-[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
-[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
-[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
-[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_INSTANTIATE
-[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
-[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_RESTRICTED
-[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
-[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
-[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
-[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
-[StrategyProperty]VBT_PHASE=VBT_SYM_EX
-[Strategy]ActiveStrategy=JavaCardDLStrategy
-[Strategy]MaximumNumberOfAutomaticApplications=500
-[Strategy]Timeout=-1
-"
+    "Choice" : {
+        "JavaCard" : "JavaCard\:off",
+        "Strings" : "Strings\:on",
+        "assertions" : "assertions\:on",
+        "bigint" : "bigint\:on",
+        "floatRules" : "floatRules\:strictfpOnly",
+        "initialisation" : "initialisation\:disableStaticInitialisation",
+        "intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules\:full",
+        "javaLoopTreatment" : "javaLoopTreatment\:efficient",
+        "javacard" : "javacard:jcOff",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal\:off",
+        "methodExpansion" : "methodExpansion\:noRestriction",
+        "modelFields" : "modelFields\:showSatisfiability",
+        "moreSeqRules" : "moreSeqRules\:off",
+        "nullPointerPolicy" : "nullPointerPolicy:nullCheck",
+        "permissions" : "permissions\:off",
+        "programRules" : "programRules\:Java",
+        "reach" : "reach\:on",
+        "runtimeExceptions" : "runtimeExceptions\:allow",
+        "sequences" : "sequences\:on",
+        "stringRules" : "stringRules:withoutStringPool",
+        "throughout" : "throughout:toutOn",
+        "transactionAbort" : "transactionAbort:abortOn",
+        "transactions" : "transactions:transactionsOn",
+        "wdChecks" : "wdChecks\:off",
+        "wdOperator" : "wdOperator\:L"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+        
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+            
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 500,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_OFF",
+            "LOOP_OPTIONS_KEY" : "LOOP_EXPAND",
+            "METHOD_OPTIONS_KEY" : "METHOD_EXPAND",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_INSTANTIATE",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
 }
 
 \javaSource ".";