I think what a side-effect is depends on what the observer is interested in when running the program. In an operational semantics, you would perhaps make such side-effects explicit by labelling certain kinds of transitions with an Event such as “asks for a new ref cell”, “reads from a ref cell”, “launches missiles”, “terminates” etc.
Over the course of the program execution, the observer can collect these events and then compare the event log of different traces. If the observer decides that ref cells are boring, then the new, read and write events aren’t a side effect and hence not collected. (The decision not to care for ref cells might still make a difference when one trace launches a missile when the other doesn’t simply because of different contents of a ref cell. Which is pretty much why Haskellers consider reading and writing to ref cells a side-effect.)
See also What is a good formal definition of purity? - #21 by sgraf in that regard.
If the observer doesn’t care whether the SMT solver is run and the result of doing so isn’t otherwise observable compared to running a pure function instead, then it’s not a side-effect. By contrast, if the SMT solver reads and writes non-existant configuration files and whatnot, the observer often questions whether the program is actually free of side-effects.