Is a software bug always a logical contradiction?

While doing my studies on propositional logic i came up with the following question:

Is a software bug always a logical contradiction between the program and the specification?

Consider the following example: Our specification tells us that "we do action C iff premise A and B are true".

Which is implemented as follows:

main ()
  if A then C
  if B then C

Clearly one can see that the specification does not fit the implementation since (consider the program above) "we do C iff the premise A or the premise B is true".

Expressing our specification and our program as propositional formulas we get the following equation:

We transform our specification to CNF and apply the resolution calculus and now we can easily see that the very first clause contradicts with the very last clause. Therefore this formula is not satisfiable and therefore our specification contradicts our implementation.

My questions are now (since the above was only an example):

Is this true for every software bug assuming a complete documentation?

and if so:

If we convert a complete specification to propositional formulas could we automate the process of software bug finding?

To answer my own question: This is called "Model Checking" and is very common in computer science in large companies like Intel to check whether hardware is actually doing what it is supposed to do.

Recently model checking started to occur more and more in software development as well. For example NASA and Microsoft are using this technology to quite some extend.

In its base form it works as follows: The specification is converted to logical statements and a compiler translates a given software program to a tree-like structure called "Kripke Structure". Model checkers take these as input and give either a counterexample for which the specification is incomplete or emit a truth value.

https://en.wikipedia.org/wiki/Model_checking