obfuscating and benchmark attributes

[DavidDeharbe]

Command-line option -obfuscate should be handle differently the values of pre-defined benchmark attributes, e.g.

(set-logic QF_UFLRA)
(set-info :source | Benchmark generated by veriT |)
(set-info :smt-lib-version 2.0)
(set-info :status unsat)
(declare-fun x () Real)
(declare-fun f (Real) Real)
(assert (=> (> x 0) (< (f x) 0)))
(assert (=> (< x 0) (> (f x) 0)))
(assert (= (f x) 0))
(assert (not (= x 0)))
(check-sat)
(exit)

yields

<pre>
(set-logic QF_UFLRA)
(set-info :source S0)
(set-info :smt-lib-version 2.0)
(set-info :status S1)
(declare-fun S2 () Real)
(declare-fun S3 (Real) Real)
(assert (=> (> S2 0) (< (S3 S2) 0)))
(assert (=> (< S2 0) (> (S3 S2) 0)))
(assert (= (S3 S2) 0))
(assert (not (= S2 0)))
(check-sat)
(exit)

For the :source attribute, it should be either:

• removed,
• replaced by "produced by smtpp -obfuscate",
• replaced by a user-defined string.

For the :status attribute, it should be either:

• kept,
• removed,
• any of the above, at the discretion of the user.