Support --values-refine with --k-induction

If --values-refine is on, we first try the intervals domain and then the
zones domain. Until now, this has been supported for AI only, now
support for k-induction, too.

This requires some tests to use --intervals instead of --values-refine
since the zones invariant inference takes too long.

Author: viktormalik

regression/heap-data/shared_mem1_false/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---heap --values-refine --k-induction
+--heap --intervals --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/kiki/hard2_unwindbound5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---heap --values-refine --k-induction --competition-mode
+--heap --intervals --k-induction --competition-mode
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*FAILURE$

src/2ls/summary_checker_kind.cpp

@@ -44,6 +44,21 @@ resultt summary_checker_kindt::operator()()
     {
       summarize(goto_model);
       result=check_properties();
+
+      if(result == resultt::UNKNOWN &&
+         options.get_bool_option("values-refine") &&
+         options.get_bool_option("intervals"))
+      {
+        // Now try with zones
+        summary_db.mark_recompute_all();
+        options.set_option("intervals", false);
+        options.set_option("zones", true);
+        summarize(goto_model);
+        result = check_properties();
+        // Reset back to intervals (for the next unwinding)
+        options.set_option("intervals", true);
+        options.set_option("zones", false);
+      }
     }
 
     if(result==resultt::PASS)