The arguments for check-sat and check-sat-using are not the same. While check-sat takes a set of assumptions (Boolean literals), check-sat-using expects a tactic that is to be applied to the current goal (like the 'apply' command), it does not take assumptions. The difference between apply and check-sat-using is that the latter applies the tactic and then checks whether the result is the empty goal or a false
goal. (For more information about goals and tactics in Z3 see the strategies tutorial.)
For this particular example, I think it would be easiest to assert assum1
into the goal before you apply qfnra-nlsat (which means you would have to construct a new goal if any of the assumptions change).
The nlsat tactic is also applied by default if the problem is in QF_NRA, but it might require an explicit
(set-logic QF_NRA)
in the beginning of the file to make sure that it is applied.