NonlinWork: formatting fix

Author: BritikovKI

test/regression/base/arithmetic/miniexample10.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b))

test/regression/base/arithmetic/miniexample2.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))

test/regression/base/arithmetic/miniexample3_Ok.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

test/regression/base/arithmetic/miniexample5.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (* a (+ b 5)))

test/regression/base/arithmetic/miniexample6_Ok.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

test/regression/base/arithmetic/miniexample7_Ok1.smt2

@@ -1,3 +1,4 @@
+(set-option :produce-models true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)