update tests for recent updates. disable model hints until available …

…in yices2 master.

src/smt/d4y2/d4y2_info.h

@@ -33,7 +33,7 @@ struct d4y2_info {
   static void setup_options(boost::program_options::options_description& options) {
     using namespace boost::program_options;
     options.add_options()
-          ("d4y2-model-as-hint", "Use the dReal model as hint for Yices2 if Dreal is not certain.")
+          // ("d4y2-model-as-hint", "Use the dReal model as hint for Yices2 if Dreal is not certain.")
           ("d4y2-relaxed-check", "Allow relaxed check, i.e. not call Yices2 in relaxed checking mode.");
   }
 

src/smt/dreal/dreal_internal.cpp

@@ -69,8 +69,11 @@ dreal_internal::dreal_internal(expr::term_manager& tm, const options& opts)
   // some basic options
   d_config->mutable_produce_models() = true;
 
-  //default precision
-  double prec = opts.get_double("dreal-precision");
+  //default precision (only has default from command line)
+  double prec = 0.0001;
+  if (opts.has_option("dreal-precision")) {
+    prec = opts.get_double("dreal-precision");
+  }
   d_config->mutable_precision() = prec;
 
   if (opts.has_option("dreal-polytope")) {
@@ -458,7 +461,6 @@ void dreal_internal::add(expr::term_ref ref, solver::formula_class f_class) {
 
 solver::result dreal_internal::check() {
 
-
   // Set bounds if needed
   if (d_ctx_bounded) {
     TRACE("dreal") << "dreal[" << instance() << "]: bounded check, precision = " << d_ctx_bounded->config().precision() << std::endl;
@@ -481,6 +483,7 @@ solver::result dreal_internal::check() {
   }
 
   if (optional<Box> res = d_ctx->CheckSat()) {
+    TRACE("dreal") << "dreal[" << instance() << "]: checking model" << std::endl;
     // If sat then dreal returns a mapping from a variable to an interval.
     // We return sat only if all intervals are singleton
     if (save_dreal_model(*res)) {

src/smt/yices2/yices2_internal.cpp

@@ -1560,14 +1560,15 @@ void yices2_internal::generalize(smt::solver::generalization_type type, expr::mo
 }
 
 void yices2_internal::set_hint(expr::model::ref m) {
-  if (d_ctx_mcsat) {
-    // Get the yices model
-    model_t* m_y = get_yices_model(m);
-    // Give yices the model as hint
-    yices_set_model_hint(d_ctx_mcsat, m_y);
-    // Free the model
-    yices_free_model(m_y);
-  }
+  throw exception("set_hint: unsupported yet.");
+//  if (d_ctx_mcsat) {
+//    // Get the yices model
+//    model_t* m_y = get_yices_model(m);
+//    // Give yices the model as hint
+//    yices_set_model_hint(d_ctx_mcsat, m_y);
+//    // Free the model
+//    yices_free_model(m_y);
+//  }
 }
 
 void yices2_internal::gc() {

test/regress/bmc/dreal/arrowsmith_and_place_fig_3_1_page_72.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 2

test/regress/bmc/dreal/cfa_test0005.mcmt.options

@@ -1,2 +1,2 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.0001 --bmc-max 16
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.0001 --bmc-max 15
 

test/regress/bmc/dreal/collin_goriely_page_60.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 2

test/regress/bmc/dreal/dumortier_llibre_artes_ex_10_15_ii.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 1

test/regress/bmc/dreal/dumortier_llibre_artes_ex_10_9.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 1

test/regress/bmc/dreal/dumortier_llibre_artes_ex_5_1_ii.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 2

test/regress/bmc/dreal/hamiltonian_system_1.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 5

test/regress/bmc/dreal/sas13-floatitp-test1.mcmt.gold

@@ -1 +1 @@
-invalid
+unknown

test/regress/bmc/dreal/sas13-floatitp-test1.mcmt.options

@@ -1 +1 @@
---engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001
+--engine bmc --lsal-extensions --solver dreal --dreal-precision=0.001 --bmc-max 10

test/regress/kind/d4y2/unstable_unit_circle3.mcmt.options

@@ -1 +1 @@
---engine kind --solver d4y2 --lsal-extensions
+--engine kind --solver d4y2 --lsal-extensions --d4y2-relaxed-check