NonlinWork: added support for mod

usi-verification-and-security · Nov 4, 2024 · c0605cd · c0605cd
1 parent d3946a7
commit c0605cd
Show file tree

Hide file tree

Showing 11 changed files with 20 additions and 0 deletions.
diff --git a/test/regression/base/arithmetic/miniexample10.smt2 b/test/regression/base/arithmetic/miniexample10.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b))
+(assert (= (uninterp_mul 5 x) 10))
+(check-sat)
+(get-model)
+(exit)
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.err b/test/regression/base/arithmetic/miniexample10.smt2.expected.err
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.out b/test/regression/base/arithmetic/miniexample10.smt2.expected.out
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    1)
+)
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out
@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod x y)")
+
+sat
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
@@ -0,0 +1 @@
+unsat
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out
@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod 5 x)")
+
+sat
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		(error "Nonlinear operations in the formula: (mod x y)")

		sat