max_tracelength option is global, not local

[tnelson]

Example:

#lang forge
option problem_type temporal 

one sig Counter {
    var count: one Int
}
pred init { Counter.count = 0}
pred move { Counter.count' = add[Counter.count, 1] }
pred traces {
    init
    always move
}

-- expect to need 2^<bitwidth> states to loop back around and form a lasso
-- 2 Int: -2, ..., 1
-- 3 Int: -4, ..., 3
-- 4 Int: -8, ..., 7
option max_tracelength 10
test expect {
    -- Confirm extension w/o traces pred (confidence test):
    traces_1: {init and move} for 3 Int is sat 
    -- 16 is too many to loop back in 10 states
    unsat_10_4: {traces} for 4 Int is unsat
    -- however, 8 is not too many to loop back in 10 states
    sat_10_3: {traces} for 3 Int is sat
}

-- Adding this should apply to only the _later_ test cases
option max_tracelength 16
test expect {
    -- with 16 states, we have just enough to loop back
    sat_16_4: {traces} for 4 Int is sat
}

Test unsat_10_4 fails in Forge 2.1.0; if you turn on verbose 5 you'll see that the max tracelength sent to Pardinus is 16 for that test. If options apply in-place, I'd expect the trace length there to be 10.

[tnelson]

@bennn Example demonstrating the option-ordering question as promised. This example where the problem arise is temporal-specific, but seems likely to impact other options as well.