NonlinWork: added PR-connected regression tests

test/regression/base/arithmetic/miniexample.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul 1 2) 2))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample.smt2.expected.out

@@ -0,0 +1 @@
+sat

test/regression/base/arithmetic/miniexample1.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_LRA)
+(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
+(assert (= (uninterp_div 1 2) 0.5))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample1.smt2.expected.out

@@ -0,0 +1 @@
+sat

test/regression/base/arithmetic/miniexample2.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= x x))
+(assert (= (uninterp_mul 2 x) (+ x x)))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample2.smt2.expected.out

@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    0)
+)

test/regression/base/arithmetic/miniexample3.smt2

@@ -0,0 +1,9 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
+(assert (= x x))
+(assert (= (uninterp_mul y x) 30))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample3.smt2.expected.out

@@ -0,0 +1,9 @@
+(error "Nonlinear operations in the formula: (* x y)")
+
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    0)
+)

test/regression/base/arithmetic/miniexample3_Ok.smt2

@@ -0,0 +1,9 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
+(assert (= x x))
+(assert (= (uninterp_mul y 5) 30))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out

@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    4)
+)

test/regression/base/arithmetic/miniexample4.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_LRA)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
+(assert (= (uninterp_div y x) 20))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample4.smt2.expected.out

@@ -0,0 +1,9 @@
+(error "Nonlinear operations in the formula: (/ y x)")
+
+sat
+(
+  (define-fun x () Real
+    0)
+  (define-fun y () Real
+    0)
+)

test/regression/base/arithmetic/miniexample4_Ok.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_LRA)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b))
+(assert (= (uninterp_div y 5) (+ 3 x)))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out

@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Real
+    0)
+  (define-fun y () Real
+    15)
+)

test/regression/base/arithmetic/miniexample5.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a (+ b 5)))
+(assert (= (uninterp_mul 2 x) (+ x 15)))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample5.smt2.expected.out

@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    5)
+)

test/regression/base/arithmetic/miniexample6.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul x y) 10))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample6.smt2.expected.out

@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (* x y)")
+
+sat

test/regression/base/arithmetic/miniexample6_Ok.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul x 10) y))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out

@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    0)
+)

test/regression/base/arithmetic/miniexample7.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul x y) 10))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample7.smt2.expected.out

@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (div x y)")
+
+sat

test/regression/base/arithmetic/miniexample7_Ok.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul 10 y) x))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out

@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (div 10 y)")
+
+sat

test/regression/base/arithmetic/miniexample7_Ok1.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b))
+(assert (= (uninterp_mul y 10) x))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out

@@ -0,0 +1,7 @@
+sat
+(
+  (define-fun x () Int
+    0)
+  (define-fun y () Int
+    0)
+)