[move-prover] Report error for unsupported bit operators

This bug fix responds to issue #166 "MVP proves arbitrary
postconditions when unsupported operators exist."

I STILL DO NOT UNDERSTAND SOME OF THE BEHAVIOR.

The fix simply reports the unsupported operator as an error when it is
encountered.  This is a one line change in bytecode_translator.rs.

I added a test case tests/sources/functional/unsupported.move for this
problem.

NOTE: The previous behavior was that, when the bytecode was
encountered, the bytecode_translater emitted a comment saying the
operator was not supported, and then an "assert false".

When Boogie is run stand-alone, it generates and output.bpl.log file
with an error trace. However, the prover doesn't seem to notice this
and report it with an error trace.  The failure is worse than that
because (according to the reported bug), the prover doesn't report
errors on incorrect postconditions.

So, I think we should understand what's going on here and try to make
sure there are not other related bugs that could result in false
negatives from unreported errors.

Closes: #201

language/move-prover/boogie-backend/src/bytecode_translator.rs

@@ -1421,6 +1421,7 @@ impl<'env> FunctionTranslator<'env> {
                         );
                     }
                     BitOr | BitAnd | Xor => {
+                        env.error(&loc, "Unsupported operator");
                         emitln!(
                             writer,
                             "// bit operation not supported: {:?}\nassert false;",

language/move-prover/tests/sources/functional/unsupported.exp

@@ -0,0 +1,6 @@
+Move prover returns: exiting with condition generation errors
+error: Unsupported operator
+  ┌─ tests/sources/functional/unsupported.move:7:37
+  │
+7 │     public fun foo(i: u64): u64 { i & 0 }
+  │                                     ^

language/move-prover/tests/sources/functional/unsupported.move

@@ -0,0 +1,13 @@
+// false negatives for unsupported operators
+
+address 0x123 {
+
+  module M {
+
+    public fun foo(i: u64): u64 { i & 0 }
+
+    spec foo { ensures false; } // :(
+
+  }
+
+}