local search + incremental doesn't work

[polgreen]

@pkesseli

Local search plus incremental causes invariant violations.

Command used:

fastsynth --local-search --incremental inv0.sl

Invariant violation:

--- begin invariant violation report ---
Invariant check failed
File: local_synth_encoding.cpp:127 function: operator()
Condition: end(solution_template.functions) != it
Reason: Check return value
Backtrace:
fastsynth_new() [0x41ba29]
fastsynth_new() [0x41c801]
fastsynth_new() [0x41aeb8]
fastsynth_new() [0x475a03]
fastsynth_new() [0x450370]
fastsynth_new() [0x474ab5]
fastsynth_new() [0x44274c]
fastsynth_new() [0x44855e]
fastsynth_new() [0x44876e]
fastsynth_new() [0x477ee1]
fastsynth_new() [0x47b73e]
fastsynth_new() [0x4319c5]
fastsynth_new() [0x434ad4]
fastsynth_new() [0x42801d]
fastsynth_new() [0x40da3d]
/lib64/libc.so.6(__libc_start_main+0xf1) [0x7f81cd7c5431]
fastsynth_new() [0x41a24a]

Benchmark here:

(set-logic BV)

(synth-fun inv () (BitVec 32)
)

(define-fun implies ((a Bool)(b Bool)) Bool
    (or (not a) b)
)

(constraint
(bvult #x00000000 inv)
)

(declare-var x (BitVec 32))

(constraint
(implies (and (bvult x inv) (not (= (bvadd x #x00000001) #x0000000a))) (not (= (bvadd x #x00000001) #x000000ff)))
)

(constraint
(implies (and (bvult x inv) (not (= (bvadd x #x00000001) #x0000000a))) (bvult (bvadd x #x00000001) inv))
)

(check-synth)