5 files changed, 4 insertions, 26 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9f9f36c8f..336bbdd32 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -616,8 +616,6 @@ set(regress_0_tests
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
   regress0/parser/bv_nat.smt2
-  regress0/parser/choice.cvc
-  regress0/parser/choice.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
   regress0/parser/force_logic_set_logic.smt2
diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2
index 649a792be..6c3cd378a 100644
--- a/test/regress/regress0/nl/sqrt2-value.smt2
+++ b/test/regress/regress0/nl/sqrt2-value.smt2
@@ -1,6 +1,6 @@
-; SCRUBBER: sed -e 's/choice.*/choice/'
+; SCRUBBER: sed -e 's/witness.*/witness/'
 ; EXPECT: sat
-; EXPECT: ((x (choice
+; EXPECT: ((x (witness
 (set-option :produce-models true)
 (set-logic ALL)
 (declare-fun x () Real)
diff --git a/test/regress/regress0/parser/choice.cvc b/test/regress/regress0/parser/choice.cvc
deleted file mode 100644
index e0ebac051..000000000
--- a/test/regress/regress0/parser/choice.cvc
+++ /dev/null
@@ -1,10 +0,0 @@
-% EXPECT: sat
-
-a : INT;
-b : INT;
-c : INT;
-
-ASSERT (CHOICE(x: INT): x = a) = 1;
-ASSERT (CHOICE(x: INT): x = b) = 2;
-
-CHECKSAT;
-\ No newline at end of file
diff --git a/test/regress/regress0/parser/choice.smt2 b/test/regress/regress0/parser/choice.smt2
deleted file mode 100644
index 19763e222..000000000
--- a/test/regress/regress0/parser/choice.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-(set-logic ALL)
-(set-info :status sat)
-(declare-fun a () Int)
-(declare-fun b () Int)
-(declare-fun c () Int)
-(assert (= (choice ((x Int)) (= x a)) 1))
-(assert (= (choice ((x Int)) (= x b)) 2))
-;(assert (let ((x (choice ((x Int)) true))) (and (distinct a b x)(= x c))))
-(check-sat)
-
diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
index 9bc47f925..3a4332176 100644
--- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
+++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -1,5 +1,5 @@
-; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (choice ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/'
-; COMMAND-LINE: --produce-models --model-witness-choice --no-check-models
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/'
+; COMMAND-LINE: --produce-models --model-witness-value --no-check-models
 ; EXPECT: sat
 ; EXPECT: SUCCESS
 (set-logic QF_NRA)