Yes: the idea is to assert that the values assigned by the found model are the only possible assignments, and hence it is unique. This can be done by adding one assertion that states that all the constants are NOT equal to their assigned model values.
For your example, this would be:
(assert (not (and
(= c3 3)
(= c2 9)
(= c1 1)
(= b3 5)
(= b2 2)
(= b1 8)
(= a3 4)
(= a2 6)
(= a1 7)
(= r3 6)
(= r2 72)
(= r1 55)
(= rc 27)
(= rb 1)
(= ra 38))))
(check-sat) ; unsat => no other model exists
If you try changing any of the values (e.g., change c3 = 3 to c3 = 4) this will again become satisfiable. Here's a rise@fun link to your complete example: http://rise4fun.com/Z3/nD5n
For more details on how to do this programmatically using the APIs, see these questions and answers:
Z3: finding all satisfying models
(Z3Py) checking all solutions for equation
Note that as per comments in the second linked answer, you cannot do this programmatically using just the SMT-lib frontend, you have to use an API to traverse the found model if you want to automate this process.