\settings {
"#Proof-Settings-Config-File
#Wed Jan 17 09:36:47 CET 2007
[General]SoundNotification=true
[DecisionProcedure]SmtBenchmarkArchiving=false
[View]FontIndex=2
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_NONE
[SimultaneousUpdateSimplifier]DeleteEffectLessLocations=true
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[General]SuggestiveVarNames=false
[View]ShowWholeTaclet=false
[General]ProofAssistant=false
[View]MaxTooltipLines=40
[General]DnDDirectionSensitive=true
[SimultaneousUpdateSimplifier]EagerSimplification=false
[General]StupidMode=true
[Strategy]MaximumNumberOfAutomaticApplications=1000
[Libraries]Default=acc.key-false, stringRules.key-false, deprecatedRules.key-false
[StrategyProperty]QUERY_OPTIONS_KEY=QUERY_NONE
[Choice]DefaultChoices=transactions-transactions\:transactionsOn , programRules-programRules\:Java , initialisation-initialisation\:disableStaticInitialisation , transactionAbort-transactionAbort\:abortOn , throughout-throughout\:toutOn , intRules-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:on , nullPointerPolicy-nullPointerPolicy\:nullCheck
[DecisionProcedure]SmtZipProblemDir=false
[Model]Source=1
[Choice]Choices=transactions-transactions\:transactionsOn-transactions\:transactionsOff , programRules-programRules\:ODL-programRules\:Java , throughout-throughout\:toutOff-throughout\:toutOn , initialisation-initialisation\:disableStaticInitialisation-initialisation\:enableStaticInitialisation , transactionAbort-transactionAbort\:abortOff-transactionAbort\:abortOn , intRules-intRules\:arithmeticSemanticsCheckingOF-intRules\:javaSemantics-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:safe-assertions\:off-assertions\:on , nullPointerPolicy-nullPointerPolicy\:noNullCheck-nullPointerPolicy\:nullCheck
[DecisionProcedure]SmtUseQuantifiers=true
[DecisionProcedure]=SIMPLIFY
[General]OuterRenaming=true
[Strategy]ActiveStrategy=JavaCardDLStrategy
"
}

\problem {
\<{
    int x;
    int res;
    res=x/x;
  }\> res = 1

}

\proof {
(keyLog "0" (keyUser "steffen" ) (keyVersion "0.2424"))

(branch "dummy ID"
(rule "variableDeclaration" (formula "1") (userinteraction "y"))
(rule "variableDeclaration" (formula "1") (userinteraction "y"))
(rule "assignment_division" (formula "1") (userinteraction "y"))
(rule "andRight" (formula "1") (userinteraction "y"))
(branch " Case 1"
   (rule "impRight" (formula "1") (userinteraction "y"))
   (rule "emptyModality" (formula "2") (term "1") (userinteraction "y"))
   (builtin "Update Simplification" (formula "2"))
   (rule "castDelInt" (formula "2") (term "0") (userinteraction "y"))
   (rule "cut" (inst "cutFormula=x >  0") (userinteraction "y"))
   (branch " CUT: x >  0 TRUE"
      (rule "jdiv_to_div_4" (formula "3") (term "0") (userinteraction "y"))
      (branch " Case 1"
         (rule "div_same" (formula "3") (term "0") (ifseqformula "2") (userinteraction "y"))
         (rule "eqClose" (formula "3") (userinteraction "n"))
         (rule "closeTrue" (formula "3") (userinteraction "n"))
      )
      (branch " Case 2"
         (builtin "Decision Procedure Simplify")
      )
   )
   (branch " CUT: x >  0 FALSE"
      (rule "jdiv_to_div_3" (formula "3") (term "0") (userinteraction "y"))
      (branch " Case 1"
         (rule "div_same" (formula "3") (term "0") (ifseqformula "1") (userinteraction "y"))
         (rule "eqClose" (formula "3") (userinteraction "n"))
         (rule "closeTrue" (formula "3") (userinteraction "n"))
      )
      (branch " Case 2"
         (rule "notLeft" (formula "1") (userinteraction "n"))
         (rule "inEqSimp_ltToLeq" (formula "3") (term "1") (userinteraction "n"))
         (rule "times_zero_1" (formula "3") (term "0,0,0,1") (userinteraction "n"))
         (rule "add_zero_left" (formula "3") (term "0,0,1") (userinteraction "n"))
         (rule "inEqSimp_gtRight" (formula "2") (userinteraction "n"))
         (rule "times_zero_1" (formula "1") (term "0,0") (userinteraction "n"))
         (rule "add_zero_left" (formula "1") (term "0") (userinteraction "n"))
         (rule "replace_known_left" (formula "3") (term "0") (ifseqformula "1") (userinteraction "n"))
         (rule "concrete_and_1" (formula "3") (userinteraction "n"))
         (rule "inEqSimp_leqRight" (formula "3") (userinteraction "n"))
         (rule "times_zero_1" (formula "1") (term "0,0,0") (userinteraction "n"))
         (rule "add_zero_left" (formula "1") (term "0,0") (userinteraction "n"))
         (rule "polySimp_addAssoc" (formula "1") (term "0") (userinteraction "n"))
         (rule "add_literals" (formula "1") (term "0,0") (userinteraction "n"))
         (rule "add_zero_left" (formula "1") (term "0") (userinteraction "n"))
         (rule "inEqSimp_strengthen1" (formula "1") (ifseqformula "3") (userinteraction "n"))
         (rule "add_zero_right" (formula "1") (term "1") (userinteraction "n"))
         (rule "inEqSimp_contradEq7" (formula "3") (ifseqformula "1") (userinteraction "n"))
         (rule "times_zero_1" (formula "3") (term "1,0,0") (userinteraction "n"))
         (rule "add_zero_right" (formula "3") (term "0,0") (userinteraction "n"))
         (rule "leq_literals" (formula "3") (term "0") (userinteraction "n"))
         (rule "concrete_and_2" (formula "3") (userinteraction "n"))
         (rule "false_right" (formula "3") (userinteraction "n"))
         (rule "inEqSimp_contradInEq0" (formula "1") (ifseqformula "2") (userinteraction "n"))
         (rule "qeq_literals" (formula "1") (term "0") (userinteraction "n"))
         (rule "concrete_and_2" (formula "1") (userinteraction "n"))
         (rule "closeFalse" (formula "1") (userinteraction "n"))
      )
   )
)
(branch " Case 2"
   (rule "impRight" (formula "1") (userinteraction "n"))
   (opengoal "\\<{     int x;     int res;     res=x/x;   }\\> res = 1 ")
)
)

}