Formal specification; Logical formula
If I understand correctly (and I might not), it sounds like maybe the property you are trying to prove is

$$\forall G . C_1(G) \implies (\exists x . C_2(G,x) \land C_3(G,x))$$

where $G$ ranges over all graphs and $x$ ranges over all possible assignments to the program variables.

If that's right, then you can't check this with SAT or with CBMC.  It's a second-order formula, so you need a 2QBF solver to check it.  SAT can help you check properties of the form "$\forall x . F(x)$" and properties of the form "$\exists x . F(x)$", but for properties of the form "$\forall x . \exists y . F(x,y)$" or "$\exists x . \forall y . F(x,y)$", you need 2QBF (or, more generally, QBF).  There do exist 2QBF solvers, but checking 2QBF properties is much harder than checking SAT.

An additional complication is that it sounds like you want to quantify over all graphs of all sizes.  

It sounds like you want to verify the following property: for all graphs, if C1 is true, then C2 and C3 are true.

The standard approach is to use assume and assert statements. You first write some assume statements that capture the assumption that the input graph satisfies C1. You then write some assert statements that capture the requirement that the C2 and C3 had better be true. The model checker checks whether there are any inputs that satisfy all the assume statements, and make at least one of the assertions false.

If you were going to use a SAT solver, you would search for a counterexample by writing a boolean formula C1 &amp;&amp; not(C2 and C3), then asking the SAT solver to find a satisfying assignment for that formula. If it finds one, that it has found a counterexample to your property. If the formula is unsatisfiable, then your property holds. This all assumes that you are reasoning about graphs of a fixed size.

If the graph is of arbitrary size, then the problem is much harder.  That falls beyond SAT and beyond even QBF, as both SAT and QBF relate to formulas with a fixed (constant) number of boolean variables -- but if you want to reason about arbitrary-sized graphs, there is no encoding of that into a fixed number of boolean variables.  A standard heuristic is to check the property on graphs of size N for a few small values of N (say, for N=1,2,3,4,5,6,... until you run out of patience or the solver starts taking too long).