Update test to fixed SmtShim

PrincetonUniversity · Aug 24, 2020 · 9db4b58 · 9db4b58
1 parent f6fdfa0
commit 9db4b58
Showing 1 changed file with 6 additions and 18 deletions.
diff --git a/test/t_smt_shim.cc b/test/t_smt_shim.cc
@@ -78,19 +78,15 @@ TEST_F(TestSmtShim, OpBvNeg) {
   auto neg_neg_a = -neg_a;
   auto prop = neg_neg_a != var_bv_a;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBvComplement) {
   auto com_a = ~var_bv_a;
   auto com_com_a = ~com_a;
   auto prop = com_com_a != var_bv_a;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBoolAnd) {
@@ -298,19 +294,15 @@ TEST_F(TestSmtShim, OpBvExtract) {
   auto extract_a_con_b = Extract(a_con_b, BV_SIZE - 1, 0);
   auto prop = extract_a_con_b != var_bv_b;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBvZext) {
   auto zext_a = ZExt(var_bv_a, 2 * BV_SIZE);
   auto zero_con_a = Concat(BvConst(0, BV_SIZE), var_bv_a);
   auto prop = zext_a != zero_con_a;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBvSext) {
@@ -319,19 +311,15 @@ TEST_F(TestSmtShim, OpBvSext) {
   auto zero_con_a = Concat(BvConst(0, BV_SIZE), pos_a);
   auto prop = sext_a != zero_con_a;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBvRotate) {
   auto left_rotate_1 = LRotate(var_bv_a, 1);
   auto right_rotate_back = RRotate(left_rotate_1, 1);
   auto prop = right_rotate_back != var_bv_a;
   CheckUnsatZ3(prop);
-#ifdef SMTSWITCH_TEST
-  EXPECT_DEATH(CheckUnsatSwitch(prop), ".*");
-#endif // SMTSWITCH_TEST
+  CheckUnsatSwitch(prop);
 }
 
 TEST_F(TestSmtShim, OpBoolImply) {