anchor.diff:          |> Optimiser.Utils.parseOptimisationString
   
       let bp = backendParams ()
  -    let { Approx = approx; NoSMTReduce = noSMTReduce; Reals = reals } =
  +    let { Approx = shouldApprox
  +          NoSMTReduce = noSMTReduce
  +          Reals = shouldUseRealsForInts } =
           config.backendOpts
           |> maybe (Seq.empty) Utils.parseOptionString
           |> Seq.fold
  
positive.code:                 mapMessages ModelFilterError npmNoSymbolicConstraintsR)
  
      let symproof : Result<Model<_, _>, Error> -> Result<Model<_, _>, Error> =
          bind (Core.Instantiate.Phase.run approx
                >> mapMessages Error.ModelFilterError)
      let eliminate : Result<Model<_, _>, Error> -> Result<Model<_, _>, Error>  =
          lift (Backends.Z3.eliminate reals)
  
      let backend m =
          let phase op response =
  
negative.code:     // Shorthand for the various stages available.
      let hsf = bind (Backends.Horn.hsfModel >> mapMessages Error.HSF)
      let smt rq = lift (Backends.Z3.backend rq)
      let muz3 rq =
          bind (Backends.MuZ3.run shouldUseRealsForInts rq
                >> mapMessages Error.MuZ3)
      let frontend times rq =
          Lang.Frontend.run times rq Response.Frontend Error.Frontend
      let graphOptimise =
  