Fixes to terms

thomasspriggs · thomasspriggs · commit 5ffdc7d07767 · 2021-06-16T19:02:42.000+01:00
diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp
@@ -49,7 +49,7 @@ bool smt_bool_literal_termt::value() const
 }
 
 smt_not_termt::smt_not_termt(smt_termt operand)
-  : smt_termt{ID_not, smt_bool_sortt{}}
+  : smt_termt{ID_smt_not_term, smt_bool_sortt{}}
 {
   INVARIANT(
     operand.get_sort() == smt_bool_sortt{},
diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h
@@ -118,6 +118,7 @@ class smt_bit_vector_constant_termt : public smt_termt
 
 class smt_function_application_termt : public smt_termt
 {
+public:
   smt_function_application_termt(
     smt_sortt return_sort,
     irep_idt function_identifier,

Original file line number	Diff line number	Diff line change
`@@ -49,7 +49,7 @@ bool smt_bool_literal_termt::value() const`
`49`	`49`	`}`
`50`	`50`
`51`	`51`	`smt_not_termt::smt_not_termt(smt_termt operand)`
`52`		`- : smt_termt{ID_not, smt_bool_sortt{}}`
	`52`	`+ : smt_termt{ID_smt_not_term, smt_bool_sortt{}}`
`53`	`53`	`{`
`54`	`54`	`INVARIANT(`
`55`	`55`	`operand.get_sort() == smt_bool_sortt{},`
Original file line number	Diff line number	Diff line change
`@@ -118,6 +118,7 @@ class smt_bit_vector_constant_termt : public smt_termt`
`118`	`118`
`119`	`119`	`class smt_function_application_termt : public smt_termt`
`120`	`120`	`{`
	`121`	`+public:`
`121`	`122`	`smt_function_application_termt(`
`122`	`123`	`smt_sortt return_sort,`
`123`	`124`	`irep_idt function_identifier,`