don't solve again if refine(query) returns the same query

[karmacoma-eth]

as is the case in this test:

    function test_expRefinement(uint256 x) external {
        vm.assume(x != 0);

        unchecked {
            assert(x ** 4 != 0);
        }
    }

[karmacoma-eth]

with #437:

halmos --root ~/projects/halmos-sandbox --function test_expRefinement --verbose --solver-command "jsi --sequence yices" 
[⠢] Compiling...
No files changed, compilation skipped

Running 1 tests for test/78_expRefinement.t.sol:Test78
setup: 0.01s (decode: 0.01s)
Executing test_expRefinement
Generating SMT queries in /tmp/test_expRefinement-8d6b3f3d00c743c5b0c86f5117097753
Found potential path (id: 0)
Panic(0x01) 
Checking path condition path_id=0
# of potential paths involving assertion violations: 1 / 1 (--solver-threads 20)
  Checking with external solver process
    jsi --sequence yices /tmp/test_expRefinement-8d6b3f3d00c743c5b0c86f5117097753/0.smt2 > /tmp/test_expRefinement-8d6b3f3d00c743c5b0c86f5117097753/0.smt2.out
  Checking again with refinement
    Refinement did not change the query, no need to solve again
WARNING  Counterexample (potentially invalid): ∅                                                                                                                                                                                                                                         
         (see https://github.com/a16z/halmos/wiki/warnings#counterexample-invalid)                                                                                                                                                                                                       
[FAIL] test_expRefinement(uint256) (paths: 1, time: 0.22s (paths: 0.11s, models: 0.11s), bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 0.24s

[time] total: 1.53s (build: 0.72s, load: 0.56s, tests: 0.24s)

Note the Refinement did not change the query, no need to solve again line (good)

If we invoke it with --smt-exp-by-const 4, then the exponentiation is replaced with a bunch of bvmuls, and refinement does change the query, and so it runs again and finds the counterexample (good)