From bc244648b750fb6d4f1619e64297a48e9b7b66c4 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <ahmed.irfan@sri.com>
Date: Wed, 15 Nov 2023 22:42:48 -0800
Subject: [PATCH] test example

---
 .../mcsat/nra/test_var_order_option.smt2      | 31 +++++++++++++++++++
 .../mcsat/nra/test_var_order_option.smt2.gold |  1 +
 2 files changed, 32 insertions(+)
 create mode 100644 tests/regress/mcsat/nra/test_var_order_option.smt2
 create mode 100644 tests/regress/mcsat/nra/test_var_order_option.smt2.gold

diff --git a/tests/regress/mcsat/nra/test_var_order_option.smt2 b/tests/regress/mcsat/nra/test_var_order_option.smt2
new file mode 100644
index 000000000..950c140a1
--- /dev/null
+++ b/tests/regress/mcsat/nra/test_var_order_option.smt2
@@ -0,0 +1,31 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoC () Real)
+(declare-fun skoS () Real)
+(declare-fun skoX () Real)
+
+(set-option :yices-mcsat-var-order (skoX skoC))
+
+(assert (let ((?v_1 (<= skoX 0)) (?v_0 (* skoC (/ (- 235) 42)))) (and (<= skoS ?v_0) (and (not ?v_1) (and (or (<= ?v_0 skoS) ?v_1) (and (= (* skoS skoS) (+ 1 (* skoC (* skoC (- 1))))) (and (<= skoX 289) (<= 0 skoX))))))))
+
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/test_var_order_option.smt2.gold b/tests/regress/mcsat/nra/test_var_order_option.smt2.gold
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/tests/regress/mcsat/nra/test_var_order_option.smt2.gold
@@ -0,0 +1 @@
+sat