From c0605cdc2e3db5bf005a35801849add5e2ec244e Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 4 Nov 2024 11:11:32 +0100 Subject: [PATCH] NonlinWork: added support for mod --- test/regression/base/arithmetic/miniexample10.smt2 | 7 +++++++ .../base/arithmetic/miniexample10.smt2.expected.err | 0 .../base/arithmetic/miniexample10.smt2.expected.out | 5 +++++ .../base/arithmetic/miniexample8.smt2.expected.err | 0 .../base/arithmetic/miniexample8.smt2.expected.out | 3 +++ .../base/arithmetic/miniexample8_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample8_Ok.smt2.expected.out | 1 + .../base/arithmetic/miniexample8_Ok2.smt2.expected.err | 0 .../base/arithmetic/miniexample8_Ok2.smt2.expected.out | 1 + .../base/arithmetic/miniexample9.smt2.expected.err | 0 .../base/arithmetic/miniexample9.smt2.expected.out | 3 +++ 11 files changed, 20 insertions(+) create mode 100644 test/regression/base/arithmetic/miniexample10.smt2 create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.out diff --git a/test/regression/base/arithmetic/miniexample10.smt2 b/test/regression/base/arithmetic/miniexample10.smt2 new file mode 100644 index 000000000..53394539e --- /dev/null +++ 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) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.err b/test/regression/base/arithmetic/miniexample10.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.out b/test/regression/base/arithmetic/miniexample10.smt2.expected.out new file mode 100644 index 000000000..264125822 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample10.smt2.expected.out @@ -0,0 +1,5 @@ +sat +( + (define-fun x () Int + 1) +) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out new file mode 100644 index 000000000..aa2d0cf74 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (mod x y)") + +sat \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out new file mode 100644 index 000000000..48cf80874 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out @@ -0,0 +1 @@ +unsat \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out new file mode 100644 index 000000000..30d440c39 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out @@ -0,0 +1 @@ +sat \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out new file mode 100644 index 000000000..8043736ab --- /dev/null +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (mod 5 x)") + +sat \ No newline at end of file