simplify

NikolajBjorner · NikolajBjorner · commit 908254752b85 · 2019-10-09T15:28:28.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
@@ -1232,15 +1232,10 @@ namespace smt {
             else if (ctx.e_internalized(m)) {
                 ADD_OCC(m);
             }
-            else if (!ctx.e_internalized(m)) {
+            else {
                 ctx.internalize(m, false);
                 ADD_OCC(m);
             }
-            else {
-                TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
-                UNREACHABLE();
-                return;
-            }
         }
 
         // Update the number of occurrences in the result vector.

Original file line number	Diff line number	Diff line change
`@@ -1232,15 +1232,10 @@ namespace smt {`
`1232`	`1232`	`else if (ctx.e_internalized(m)) {`
`1233`	`1233`	`ADD_OCC(m);`
`1234`	`1234`	`}`
`1235`		`- else if (!ctx.e_internalized(m)) {`
	`1235`	`+ else {`
`1236`	`1236`	`ctx.internalize(m, false);`
`1237`	`1237`	`ADD_OCC(m);`
`1238`	`1238`	`}`
`1239`		`- else {`
`1240`		`- TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);`
`1241`		`- UNREACHABLE();`
`1242`		`- return;`
`1243`		`- }`
`1244`	`1239`	`}`
`1245`	`1240`
`1246`	`1241`	`// Update the number of occurrences in the result vector.`