I think it's much better than brute force search. The example above produces the following code:

  val (hours, minutes, seconds) = {
    val loc1 = secnum div 3600
    val num2 = secnum + ((−3600) ∗ loc1)
    val loc2 = min(num2 div 60, 59)
    val loc3 = secnum + ((−3600) ∗ loc1) + (−60 ∗ loc2)
    (loc1, loc2, loc3)
  }

Note that it works for constraints expressed in (parameterized) linear arithmetic and with operations on sets (like taking cardinality, union, intersection...).