Revert "Use unknown as expected verdicts (#611)"

A Boogie file is either safe or unsafe.

This reverts commit 86f7848.

trunk/examples/programs/quantifier/regression/bpl/AuxVarInCall.bpl

@@ -1,4 +1,4 @@
-// #Unknown
+// #Safe
 // Reveals bug of issue #441.
 // https://github.com/ultimate-pa/ultimate/issues/441
 // Computations of pre, sp, wp, and interprocedural sequential composition

trunk/examples/programs/regression/bpl/toolDirectives/Overapproximation.bpl

@@ -1,12 +1,17 @@
-//#Unknown
+//#Safe
 // Author: [email protected]
 // Date: 2015-08-14
 //
 // Test for the overapproximation tool directive that we pass to Ultimate via attributes.
 //
 // Our wiki says the following.
-// If a function func has the attribute {:overapproximation "bar"} our model checkers will never output a counterexample that contains func.
-// Instead our model checkers might say unknown and that an overapproximation of bar is the reason for saying unknown. 
+// If a function func has the attribute {:overapproximation "bar"} our model checkers will never output a counterexample that contains func. Instead our model checkers might say unknown and that an overapproximation of bar is the reason for saying unknown. 
+//
+// In fact, this program is not safe (resp. it is only safe with respect to
+// the assumption that the semantics of ~bitwiseAnd is a bitwise complement for
+// a two's complement representation of the inputs), but we use this file that
+// Ultimate does not output the result UNSAFE.
+
 
 function { :overapproximation "bitwiseAnd" } ~bitwiseAnd(in0 : int, in1 : int) returns (out : int);