deeply nested expression evaluation test

Author: jezhiggins

regression/goto-analyzer-simplify/simplify-deeply-nested-expression/main.c

@@ -0,0 +1,42 @@
+int nondet_int(void);
+
+struct MH
+{
+  int s;
+  int t;
+  int to;
+  int su;
+};
+
+int main(void)
+{
+  int l = nondet_int();
+  int s = nondet_int();
+  int n = nondet_int();
+  int o = nondet_int();
+  int nt = nondet_int();
+  int ns = nondet_int();
+
+  struct MH mh;
+  mh.s = nondet_int();
+  mh.t = nondet_int();
+  mh.to = nondet_int();
+  mh.su = nondet_int();
+
+  int result =
+    ((l >= mh.s ? 1 : 0) &
+     (((mh.s >= s ? 1 : 0) &
+       (((n >= mh.t ? 1 : 0) &
+         (((mh.t >= o ? 1 : 0) & ((((int)mh.to == (int)nt ? 0 : 1) &
+                                   ((int)mh.su == (int)ns ? 0 : 1)) == 0
+                                    ? 0
+                                    : 1)) == 0
+            ? 0
+            : 1)) == 0
+          ? 0
+          : 1)) == 0
+        ? 0
+        : 1)) == 0;
+
+  assert(result = 0);
+}

regression/goto-analyzer-simplify/simplify-deeply-nested-expression/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--vsd
+^SIGNAL=0$
+^EXIT=0$
+--
+--
+This expression is derived from a real system under test. Due to inadvertent reevaluation of expression operands, all expression evaluations had geometric complexity (even more so in the presence of TOP values). This particular expression took nearly two hours to evaluate. Reworking to prevent repeated reevaluation brings this down to a few tenths.
+See https://github.com/diffblue/cbmc/pull/6290
+If this test appears to hang, the constant_evaluator is probably your first port of call.